Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Appearance settings

Commit a63c327

Browse filesBrowse files
tglsfdctglsfdc
committed
Fix test_predtest's idea of what weak refutation means.
I'd initially supposed that predicate_refuted_by(..., true) ought to say that "A refutes B" means "non-falsity of A implies non-truth of B". But it seems better to define it as "truth of A implies non-truth of B". This is more useful in the current system, slightly easier to prove, and in closer correspondence to the existing code behavior. With this change, test_predtest no longer claims that any existing test cases show false proof reports, though there still are cases where we could prove something and fail to. Discussion: https://postgr.es/m/5983.1520487191@sss.pgh.pa.us
1 parent 960df2a commit a63c327
Copy full SHA for a63c327

File tree

Expand file treeCollapse file tree

2 files changed

+11
-9
lines changed
Open diff view settings
Filter options
Expand file treeCollapse file tree

2 files changed

+11
-9
lines changed
Open diff view settings
Collapse file

‎src/test/modules/test_predtest/expected/test_predtest.out‎

Copy file name to clipboardExpand all lines: src/test/modules/test_predtest/expected/test_predtest.out
+5-7Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,6 @@ select * from test_predtest($$
119119
select x is not true, x
120120
from booleans
121121
$$);
122-
WARNING: weak_refuted_by result is incorrect
123122
-[ RECORD 1 ]-----+--
124123
strong_implied_by | f
125124
weak_implied_by | f
@@ -128,7 +127,7 @@ weak_refuted_by | t
128127
s_i_holds | f
129128
w_i_holds | f
130129
s_r_holds | t
131-
w_r_holds | f
130+
w_r_holds | t
132131

133132
select * from test_predtest($$
134133
select x, x is not true
@@ -176,7 +175,6 @@ select * from test_predtest($$
176175
select x is unknown, x
177176
from booleans
178177
$$);
179-
WARNING: weak_refuted_by result is incorrect
180178
-[ RECORD 1 ]-----+--
181179
strong_implied_by | f
182180
weak_implied_by | f
@@ -185,7 +183,7 @@ weak_refuted_by | t
185183
s_i_holds | f
186184
w_i_holds | f
187185
s_r_holds | t
188-
w_r_holds | f
186+
w_r_holds | t
189187

190188
select * from test_predtest($$
191189
select x, x is unknown
@@ -214,7 +212,7 @@ weak_refuted_by | f
214212
s_i_holds | f
215213
w_i_holds | f
216214
s_r_holds | t
217-
w_r_holds | f
215+
w_r_holds | t
218216

219217
select * from test_predtest($$
220218
select x, x is null
@@ -650,7 +648,7 @@ weak_refuted_by | f
650648
s_i_holds | f
651649
w_i_holds | f
652650
s_r_holds | t
653-
w_r_holds | f
651+
w_r_holds | t
654652

655653
select * from test_predtest($$
656654
select x is null, int4lt(x,8)
@@ -664,7 +662,7 @@ weak_refuted_by | f
664662
s_i_holds | f
665663
w_i_holds | f
666664
s_r_holds | t
667-
w_r_holds | f
665+
w_r_holds | t
668666

669667
select * from test_predtest($$
670668
select x is not null, x < 'foo'
Collapse file

‎src/test/modules/test_predtest/test_predtest.c‎

Copy file name to clipboardExpand all lines: src/test/modules/test_predtest/test_predtest.c
+6-2Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -104,14 +104,18 @@ test_predtest(PG_FUNCTION_ARGS)
104104
c2 = 'f';
105105

106106
/* Check for violations of various proof conditions */
107+
108+
/* strong implication: truth of c2 implies truth of c1 */
107109
if (c2 == 't' && c1 != 't')
108110
s_i_holds = false;
111+
/* weak implication: non-falsity of c2 implies non-falsity of c1 */
109112
if (c2 != 'f' && c1 == 'f')
110113
w_i_holds = false;
114+
/* strong refutation: truth of c2 implies falsity of c1 */
111115
if (c2 == 't' && c1 != 'f')
112116
s_r_holds = false;
113-
/* XXX is this the correct definition for weak refutation? */
114-
if (c2 != 'f' && c1 == 't')
117+
/* weak refutation: truth of c2 implies non-truth of c1 */
118+
if (c2 == 't' && c1 == 't')
115119
w_r_holds = false;
116120
}
117121

0 commit comments

Comments
0 (0)
Morty Proxy This is a proxified and sanitized view of the page, visit original site.