line-aware synthesis producing incorrect results

[Geremia]

When doing line-aware synthesis on the choose (Ch) function:

module Ch(out o, in x, in y, in z)
  o ^= ((x & y) ^ (~x & z))

the output variable o isn't correct:

expected: 11011001001110100010100101000000
actual:   01000001000000000000100100000000

for these (or any other) test values:

"x": "10111010111111110011001011001010",
"y": "11011101001110101010110101110001",
"z": "11001011111111000010100110000000"

Cost-aware synthesis produces correct results.

mqt-core                3.3.3
mqt-syrec               2.0.1.dev68+g83223c633.d20251229

[Geremia]

This module also doesn't produce the correct output with line-aware synthesis, but it does with cost-aware synthesis:

module s0(out o, in a, in b, in x)
  o ^= (a ^ (b ^ (x >> 3)))

expected: 01010001101010100101101110001110
actual:   00010011001111111100010110111011

Input values:

"a": "01000010100101011001111000110101",
"b": "01011111100101000001111001010011",
"x": "10001001100101010111101101111101"

[TooMuchDakka]

The issue when synthesizing the Ch module with the line aware synthesis algorithm is the following:

1. Prior to the synthesis of an assignment using the line aware synthesis the latter checks whether the assignment fullfills a set of preconditions. If these conditions do not hold then the synthesis of the assignment is delegated to the base class (i.e. SyrecSynthesis::onStatement)
2. With the current code structure certain member variables shared between all synthesis algorithms but only really used in the line aware synthesis are set while synthesizing the right-hand side expression (rhs) of the assignment.
3. After the rhs expression was synthesized the SyrecSynthesis::onStatement(const AssignStatement& statement) function will perform the synthesis of the assignment operation by calling the potentially overwritten SyrecSynthesis::assign<OP> functions which in case of the line aware synthesis will call LineAwareSynthesis::assignExor whos implementation requires that the logic of the line aware synthesis was applied during the synthesis of the rhs expression but that we deliberately skipped in 1.

The same issues should also effect all assignment statements synthesized with the line aware synthesis in which the assignment operation is equal to the binary operation of the parent binary expression of the right-hand side of the synthesized assignment (i.e. for assignments of the form a += (E1 + E2), a -= (E1 - E2), a ^= (E1 ^ E2)). Thus the same issue should also cause the incorrect results in the s0 module.

Note: An issue in the generation of the subassignments in the line aware synthesis is still not resolved (see #280)

[Geremia]

@TooMuchDakka

Note: An issue in the generation of the subassignments in the line aware synthesis is still not resolved (see #281)

Do you mean #280?