EvalAnd: (a||b||c) && (b||!a) simplifies to b
メンテナーはふだん 1 日以内に返信
まだ誰も着手していません。
評価
調査の方向性
Start in the EvalAnd class, at the block commented 'A || B && A || !B ==> A', which handles OR-OR reduction. Work through the two counter-examples in the issue by hand to see which case the check accepts wrongly. Done means the reduction only fires when both ORs share all components except exactly one complementary pair, and the issue's examples evaluate to the same truth value before and after simplification.
索引モデルが issue の本文から書いたものです。
説明
EvalAnd: (a||b||c) && (b||!a) simplifies to b
The OR-OR reduction in EvalAnd (commented A || B && A || !B ==> A) produces non-equivalent results.
Expression a = ..., b = ..., c = ..., x = ...; // boolean local variables
runtime.and(runtime.or(a, b, c), runtime.or(b, runtime.negate(a)))
// result: b
// expected: b || !a && c (or left as is)
// counter-example: a=false, b=false, c=true -> input is true, result is false
runtime.and(runtime.or(a, b, x), runtime.or(runtime.negate(a), runtime.negate(b), x))
// result: x
// counter-example: a=true, b=false, x=false -> input is true, result is false
(a||b) && (b||!a) → b is correct; the reduction is only valid in that shape.
Cause
In EvalAnd, the block under // A || B && A || !B ==> A checks every component of the current OR against the previous one (equal, or opposite). It does not check the converse: components of the previous OR that the current one does not mention (c above) are dropped. Nor does it limit the number of opposite pairs to one; with two (a/!a, b/!b), the remaining common part is not implied.
The resolution (A || X) && (!A || X) ==> X holds when both ORs have the same components apart from exactly one complementary pair.
Impact
In a downstream analyzer, the condition
(NUMBER==p || LONG==p || SINGLE!=p) && (LONG==p || NUMBER!=p) && DOUBLE==p
(static final int constants; satisfiable with p == DOUBLE) was reduced to false or to DOUBLE==p && LONG==p depending on operand order, so code guarded by it was dropped as dead.
Reproduced on 0.9.5-alpha.9 and on current devel (EvalAnd unchanged).
- 主要言語
- Java
- スター
- 1
- フォーク
- 1
- 平均マージ
- 1時間 44分
- マージ済み PR（30日）
- 6
環境構築
- Dockerfile・Docker Compose ファイルなし
- プルリクエストのテンプレートあり
- コントリビューションガイドを読む
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
CodeLaser/maddi のほかの issue
-
難易度 2/5 1〜3時間 初心者へのやさしさ 78/100
CodeLaser/maddi#166 · コメント 3 件 ·
メンテナーはふだん 1 日以内に返信
-
build/ci good first issue
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
メンテナーはふだん 1 日以内に返信
-
難易度 5/5 1週間以上 初心者へのやさしさ 14/100
メンテナーはふだん 1 日以内に返信
-
難易度 4/5 3〜5日 初心者へのやさしさ 35/100
メンテナーはふだん 1 日以内に返信
-
難易度 4/5 3〜5日 初心者へのやさしさ 48/100
メンテナーはふだん 1 日以内に返信
CodeLaser/maddi の issue をすべて見る
似ている issue
-
難易度 2/5 1〜3時間 初心者へのやさしさ 82/100
AtlasOfLivingAustralia/species-lists#882 ·
メンテナーはふだん 1 日以内に返信
-
Type/Bug
難易度 2/5 1〜3時間 初心者へのやさしさ 62/100
ballerina-platform/ballerina-library#9458 ·
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 68/100
winder/Universal-G-Code-Sender#3242 ·
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 68/100
PCL-Community/PCL-CE#3767 ·
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 62/100