EvalAnd: (a||b||c) && (b||!a) simplifies to b

Cerrado
  • ¿Algo no está bien?
#117 0 comentarios 0 reacciones 0 asignados Ver en GitHub

Los mantenedores suelen responder en 1 día

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
3/5
Tiempo estimado
Medio día
Aptitud para principiantes
62/100
Tipo de issue
Error
Claridad
Bien especificado
Estado de actividad
Activo
Stack tecnológico
java
Área
compilers

Línea de trabajo

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.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

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).

Lenguaje dominante
Java
Estrellas
1
Forks
1
Merge medio
1 h 44 min
PR fusionados (30 d)
6

Preparar el entorno

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de CodeLaser/maddi

Todos los issues de CodeLaser/maddi

Issues similares

Más issues de Java

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.