Concrete backend should be able to handle extremely simple symbolic cases

[rhelmot]

• evaluating x when x == 4 should not touch z3
• evaluating y when y == x and x == 4 should not touch z3
• evaluating x when x[15:0] == 4 and x[31:16] == 5 should not touch z3
• max(x) when x <= 5 (and no other constraints on x) should not touch z3
• max(x) when x <= y and y <= 5 (and no other constraints on x and y) should not touch z3

[zardus]

We support this (and considerably more complex cases even!) with the HybridSolver, which uses the ReplacementFrontend coupled with a VSA LightFrontend. It doesn't touch Z3, but on the other hand, it executes a lot of python code, so we don't often "win" on performance.

We could probably use almost the exact same scaffold but without VSA for more speed at the cost of only handling simpler expressions.

[github-actions]

This issue has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

[github-actions]

This issue has been closed due to inactivity.