NotificationsYou must be signed in to change notification settings
Fork6
Star31

Commita63c327

committed

Fix test_predtest's idea of what weak refutation means.

I'd initially supposed that predicate_refuted_by(..., true) ought tosay 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 existingtest cases show false proof reports, though there still are caseswhere we could prove something and fail to.Discussion:https://postgr.es/m/5983.1520487191@sss.pgh.pa.us

1 parent960df2a commita63c327Copy full SHA for a63c327

File tree

2 files changed

+11

-9

lines changed

src/test/modules/test_predtest
- expected
  - test_predtest.out
- test_predtest.c

2 files changed

+11

-9

lines changed

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

Lines changed: 5 additions & 7 deletions

Original file line number	Diff line number	Diff line change
`@@ -119,7 +119,6 @@ select * from test_predtest($$`
`119`	`119`	`select x is not true, x`
`120`	`120`	`from booleans`
`121`	`121`	`$$);`
`122`		`-WARNING: weak_refuted_by result is incorrect`
`123`	`122`	`-[ RECORD 1 ]-----+--`
`124`	`123`	`strong_implied_by \| f`
`125`	`124`	`weak_implied_by \| f`
`@@ -128,7 +127,7 @@ weak_refuted_by \| t`
`128`	`127`	`s_i_holds \| f`
`129`	`128`	`w_i_holds \| f`
`130`	`129`	`s_r_holds \| t`
`131`		`-w_r_holds \|f`
	`130`	`+w_r_holds \|t`
`132`	`131`
`133`	`132`	`select * from test_predtest($$`
`134`	`133`	`select x, x is not true`
`@@ -176,7 +175,6 @@ select * from test_predtest($$`
`176`	`175`	`select x is unknown, x`
`177`	`176`	`from booleans`
`178`	`177`	`$$);`
`179`		`-WARNING: weak_refuted_by result is incorrect`
`180`	`178`	`-[ RECORD 1 ]-----+--`
`181`	`179`	`strong_implied_by \| f`
`182`	`180`	`weak_implied_by \| f`
`@@ -185,7 +183,7 @@ weak_refuted_by \| t`
`185`	`183`	`s_i_holds \| f`
`186`	`184`	`w_i_holds \| f`
`187`	`185`	`s_r_holds \| t`
`188`		`-w_r_holds \|f`
	`186`	`+w_r_holds \|t`
`189`	`187`
`190`	`188`	`select * from test_predtest($$`
`191`	`189`	`select x, x is unknown`
`@@ -214,7 +212,7 @@ weak_refuted_by \| f`
`214`	`212`	`s_i_holds \| f`
`215`	`213`	`w_i_holds \| f`
`216`	`214`	`s_r_holds \| t`
`217`		`-w_r_holds \|f`
	`215`	`+w_r_holds \|t`
`218`	`216`
`219`	`217`	`select * from test_predtest($$`
`220`	`218`	`select x, x is null`
`@@ -650,7 +648,7 @@ weak_refuted_by \| f`
`650`	`648`	`s_i_holds \| f`
`651`	`649`	`w_i_holds \| f`
`652`	`650`	`s_r_holds \| t`
`653`		`-w_r_holds \|f`
	`651`	`+w_r_holds \|t`
`654`	`652`
`655`	`653`	`select * from test_predtest($$`
`656`	`654`	`select x is null, int4lt(x,8)`
`@@ -664,7 +662,7 @@ weak_refuted_by \| f`
`664`	`662`	`s_i_holds \| f`
`665`	`663`	`w_i_holds \| f`
`666`	`664`	`s_r_holds \| t`
`667`		`-w_r_holds \|f`
	`665`	`+w_r_holds \|t`
`668`	`666`
`669`	`667`	`select * from test_predtest($$`
`670`	`668`	`select x is not null, x < 'foo'`

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

Lines changed: 6 additions & 2 deletions

Original file line number	Diff line number	Diff line change
`@@ -104,14 +104,18 @@ test_predtest(PG_FUNCTION_ARGS)`
`104`	`104`	`c2='f';`
`105`	`105`
`106`	`106`	`/* Check for violations of various proof conditions */`
	`107`	`+`
	`108`	`+/* strong implication: truth of c2 implies truth of c1 */`
`107`	`109`	`if (c2=='t'&&c1!='t')`
`108`	`110`	`s_i_holds= false;`
	`111`	`+/* weak implication: non-falsity of c2 implies non-falsity of c1 */`
`109`	`112`	`if (c2!='f'&&c1=='f')`
`110`	`113`	`w_i_holds= false;`
	`114`	`+/* strong refutation: truth of c2 implies falsity of c1 */`
`111`	`115`	`if (c2=='t'&&c1!='f')`
`112`	`116`	`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')`
`115`	`119`	`w_r_holds= false;`
`116`	`120`	`}`
`117`	`121`

0 commit comments

Comments

(0)

Movatterモバイル変換

Navigation Menu

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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Commita63c327

File tree

2 files changed

2 files changed

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

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

0 commit comments