Incomplete normalization of a function's argument containing logical expressions

[pt7k]

1. Summary

   • Description: Bug Summary in 2 to 3 sentences.
   • When a disjunction of 3 variables and a negation of one of the variables is directly normalized in REPL it always results in 1 as expected.
   • But if the exact same expression is passed as an argument to a function it is not being evaluated to 1 and left in its raw value most of the times (below I demonstrated one possible exception showing that it can be done in some circumstances).

2. Environment

   • Tau Version: for now "v0.7-alpha" -158
   • Build Number or Date: eb3d8e5
   • Operating System: Ubuntu

3. Steps to Reproduce
   Step 1: What input did you first provide?

yes_it_is(0) := 0
is_one(1) := yes_it_is(1)
logical_one() := f(1) | g(1) | h(1) | (f(1))'
n is_one(logical_one())

logical_xyz() := x|y|z|x'
n is_one(logical_xyz())

Step 2: Any additional input to Tau?
Expected Result
is_one predicate should evaluate its argument to 1 and then match that input with its definition outputting yes_it_is(1)
Actual Result
With the expression containing functions f(1), g(1), h(1) it did not evaluate the argument and returned the raw expression.
In case of the x,y,z variables it evaluated the argument to 1 but did not match it with is_one definition so it returned its raw output with normalized argument i.e. is_one(1) instead of expected yes_it_is(1).
4. Additional Information

• Error Messages or Logs:
• Screenshots:
  

Further screenshot posted below in the Workaround section

5. Severity and Impact

   • Severity Level: Major
   • Impact on Work: It does not allow to further process any output of one function containing logical expressions as an input to another.

6. Workaround (if applicable)

   • Tell us if you found a way around this problem:
   • I was able to make this simple disjunction example evaluate to 1 and output correct result by swapping the disjuncts order so the two that are the opposites of each other are adjacent and thus somehow triggering the normalization to reduce the pair to 1 and then it could propagate further to other disjuncts making the whole expression evaluate to 1. Then is_one(1) is correctly matched with its definition and outputs yes_it_is(1) as expected for both f()g()h() and xyz examples.
   • But as demonstrated below it only works on that simple example and only if one can manipulate the input manually so more complex expressions or having dynamic input with arbitrary sequence cannot be worked around like that.

7. Contact Information
   • Name: pt7k
   • Email: Telegram @ksdjfskfh
   • Additional Notes: Any other message for the Tau Team

Submission Instructions

• Make sure to attach any input files to this bug report.
  mydemo_params_normalization1.tau.txt
  mydemo_params_normalization2.tau.txt

[LuccaT95]

Dear pt7k,

thank you for the report. We have identified your reported bug and will work on fixing it shortly.

Best,
Lucca

[pt7k]

Thanks Lucca,
that would be great.

Best,
pt7k