EvalAnd: (a||b||c) && (b||!a) simplifies to b
Nobody has claimed this yet.
Assessment
- Difficulty
- 3/5
- Estimated time
- Half a day
- Newbie friendliness
- 62/100
Research direction
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.
Written by the indexing model from the issue text.
Description
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).
- Dominant language
- Java
- Stars
- 1
- Forks
- 1
- Avg merge
- 2h 51m
- Merged PRs (30d)
- 3
Getting set up
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from CodeLaser/maddi
-
build/ci good first issue
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
-
Difficulty 4/5 3-5 days Newbie friendliness 48/100
-
Difficulty 4/5 3-5 days Newbie friendliness 45/100
-
enhancement
Difficulty 3/5 1-2 days Newbie friendliness 45/100
-
Java → C# translation: an idiomatic C# printer driven by the modification and nullability analysesOpenenhancement extension front-end:csharp
Difficulty 5/5 Over a week Newbie friendliness 8/100
Similar issues
-
[BUG] 增量 SSE 解析器未识别单独 CR 换行，导致事件无法及时交付Possibly taken @king-wwwhhh claimed this today. Open
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
langchain4j/langchain4j#6669 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
OpenAPITools/openapi-generator#25237 ·
Maintainers usually reply within 1 day
-
needs-area-label
Difficulty 2/5 1-3 hours Newbie friendliness 82/100
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
quelea-projection/Quelea#711 ·
-
bug pdd
Difficulty 2/5 Under an hour Newbie friendliness 67/100
objectionary/eo#9450 ·
Maintainers usually reply within 1 day