[FEATURE] Better constant propagation

[konnov]

The current optimizer propagates constants, but fails to do so in some cases. For example:

---------------------------- MODULE Opt1 -------------------------------------  
VARIABLES S

A == "Foo"

Init ==
    S = 0

Next ==
    IF A = "Foo"
    THEN S' = 1
    ELSE S' = 2
==============================================================================

The output after the optimization step (as can be seen in out-opt.tla), is like this:

----- MODULE Opt1 -----                                                         
  
VARIABLE S

Init$0 == S' := 0

Next$0 == "Foo" = "Foo" /\ S' := 1

Next$1 == ~("Foo" = "Foo") /\ S' := 2
===============

It is not clear, why the optimizer did not rewrite "Foo" = "Foo" into TRUE.

The optimizer can be found in at.forsyte.apalache.tla.pp.passes.OptPassImpl.

[istoilkovska]

Equality simplification is defined only for ValEx(TlaInt) and NameEx here.

[konnov]

True. That explains it :D