Reduct Zero-Subsumption Fix#439
Conversation
|
|
||
| ;; Promote Common Constraints Test | ||
| ;; !(assertEqual (reduceToElegance (AND A (OR (AND (NOT B) C) (AND (NOT B))) (OR (AND (NOT C)) (AND (NOT B) (NOT D)))) (OR (AND (NOT B) C) (AND (NOT B))) (A) ()) ((AND A (NOT B) (OR (AND (NOT C)) (AND (NOT B) (NOT D)))) () True)) ;; FIX: Classic says this should be (AND) | ||
| !(assertEqual (reduceToElegance (AND A (OR (AND (NOT B) C) (AND (NOT B))) (OR (AND (NOT C)) (AND (NOT B) (NOT D)))) (OR (AND (NOT B) C) (AND (NOT B))) (A) ()) ((AND A (NOT B) (OR (AND (NOT C)) (AND (NOT B) (NOT D))) C) () True)) ;; FIX: Classic says this should be (AND) |
There was a problem hiding this comment.
We should test this with the reduce-to function and see if the output is like the classic:
(AND (OR (NOT C) (NOT D)) A (NOT B))or
(AND (OR (AND (NOT C)) (AND (NOT D))) (AND A) (AND (NOT B)))There was a problem hiding this comment.
Add the test case below or replace the test case?
There was a problem hiding this comment.
This is the value returned (AND A (NOT B) C (NOT D)) from running
!(reduce-to (AND A (OR (AND (NOT B) C) (AND (NOT B))) (OR (AND (NOT C)) (AND (NOT B) (NOT D)))))
There was a problem hiding this comment.
Never mind. This needs another check. I was hopping the results would be the same.
|
|
||
| ;; 0-Constraint Subsumption Test | ||
| ;; !(assertEqual (reduceToElegance (AND A (OR (AND A) (AND (NOT B) (OR (AND E) (AND F)))) (OR (AND C) (AND))) (OR (AND C) (AND)) (A) ()) ((AND A (OR (AND A) (AND (NOT B) (OR (AND E) (AND F))))) () False)) ;; FIX: Classic says this should be (AND (OR (AND E) (AND F)) A (NOT B) C) | ||
| !(assertEqual (reduceToElegance (AND A (OR (AND A) (AND (NOT B) (OR (AND E) (AND F)))) (OR (AND C) (AND))) (OR (AND C) (AND)) (A) ()) ((AND A (OR (AND A) (AND (NOT B) (OR (AND E) (AND F)))) C) () False)) ;; FIX: Classic says this should be (AND (OR (AND E) (AND F)) A (NOT B) C) |
There was a problem hiding this comment.
Test this with the full path using reduce-to. Classic says it should be (AND A C)
| !(assertEqual (reduceToElegance (AND (AND (NOT A) (NOT C) B (OR B (NOT A)))) (AND (NOT A) (NOT C) B (OR B (NOT A))) () ()) ((AND (AND (NOT A) (NOT C) B (OR B (NOT A)))) (AND (NOT A) (NOT C) B (OR B (NOT A))) False)) | ||
| ;; (AND A (OR B (AND C (OR D (AND E (NOT A)))))) ==> (AND A (OR B (AND C D))) | ||
| ;; !(assertEqual (reduceToElegance (AND (AND A (OR B (AND C (OR D (AND E (NOT A))))))) (AND A (OR B (AND C (OR D (AND E (NOT A)))))) () ()) ((AND (AND A C (OR B D))) (AND A C (OR B D)) False)) ;; FIX: Classic says it should be (AND (OR (AND C D) B) A) | ||
| !(assertEqual (reduceToElegance (AND (AND A (OR B (AND C (OR D (AND E (NOT A))))))) (AND A (OR B (AND C (OR D (AND E (NOT A)))))) () ()) ((AND (AND A C (OR B D))) (AND A C (OR B D)) False)) ;; FIX: Classic says it should be (AND (OR (AND C D) B) A) |
There was a problem hiding this comment.
Their outputs are not gonna be the same, but will add the test case for that below
There was a problem hiding this comment.
Yeah I know. Most of the comments are actually just for future reminder. It doesn't have to be resolved in this PR.
| !(assertEqual (reduceToElegance (AND (OR A A)) (OR A A) () ()) ((AND (OR A A)) (OR A A) False)) ;; ((AND A) () False) | ||
| ;; (AND (OR (AND A B) A C)) ==> (AND (OR (AND A B) A C)) | ||
| !(assertEqual (reduceToElegance (AND (OR (AND A B) A C)) (OR (AND A B) A C) () ()) ((AND A B) () True)) | ||
| !(assertEqual (reduceToElegance (AND (OR (AND A B) A C)) (OR (AND A B) A C) () ()) ((AND A B C) () True)) |
There was a problem hiding this comment.
Test with reduce-to because this should have been (OR A C) according to the classic.
| !(assertEqual (reduceToElegance (AND (OR A B C D C)) (OR A B C D C) () ()) ((AND (OR A B C D C)) (OR A B C D C) False)) | ||
| ;; (AND (OR A (AND B C D C))) ==> (AND (OR A (AND B C D C))) | ||
| !(assertEqual (reduceToElegance (AND (OR A (AND B C D C))) (OR A (AND B C D C)) () ()) ((AND B C D) () True)) | ||
| !(assertEqual (reduceToElegance (AND (OR A (AND B C D C))) (OR A (AND B C D C)) () ()) ((AND B C D A) () True)) |
There was a problem hiding this comment.
Okay, this pattern is too frequent to ignore any more. The classic says this should be a (OR (AND B C D) A) instead ours reduced it to (AND B C D A) essentially merging it into the AND what should have been kept as the OR's child.
There was a problem hiding this comment.
This happens on some of the above test cases as well. But they seem to have similar origin.
List: line 37: Should have been like the comment.
line 33: Should have been (OR (AND A B) C D)
line 43: Should have been (OR (AND (NOT A) B) (NOT C) (NOT D))
Yagth
left a comment
There was a problem hiding this comment.
There is one more test potential bug and few tests to conduct before marking the reduct issue resolved. But I am going to merge this one anyway. Check out the comments if you want to test them out yourself :)
Description
The zero-subsumption rule was excluding literals from its operation on the
childrenof a given POA and only considering the subexpressions, resulting in an invalid expression. Now thechildrenexpression correctly contains its literals before any operation is done.Motivation and Context
How Has This Been Tested?
Types of changes
Checklist: