Enforce use of relation TS when specified

[Po-Chun-Chien]

This PR introduces the following changes:

• Add a new option --use-rel-ts
• Make pseudo_init_and_prop() accept only relation TS
• Create the correct type of TS right at the beginning (before encoding)

The latter two are important to avoid issues arising from casting based on ts.is_functional().

In the original implementation (b19eafb), pseudo_init_and_prop() may "convert" a functional TS to a relational one.
However, since we are assigning the returned RelationalTransitionSystem back to a TransitionSystem& in pono.cpp, object slicing could cause issues in subsequent casting.
For example, if we modify pono.cpp as follows:

  // in check_prop
  if (pono_options.pseudo_init_prop_) {
    ts = pseudo_init_and_prop(ts, prop);
    if (!ts.is_functional()) {
      dynamic_cast<RelationalTransitionSystem &>(ts);
    }
  }

A std::bad_cast will be encountered (suppose --pseudo-init-prop is enabled).

[CyanoKobalamyne]

I agree with the pseudo init fixes and changes, but what is the use case for the use-rel option? I don't think we have exposed the functional-relational distinction through the CLI until now. Also, I think we might eventually want to merge the two implementations and just leave the internal flag that indicates whether the system is functional...

[Po-Chun-Chien]

I agree with the pseudo init fixes and changes, but what is the use case for the use-rel option?

I added it because I came across an interesting case where it can help improve performance when combined with the transformation introduced in #521.

That said, I haven’t evaluated it on a larger benchmark set, so I’m not certain of its overall impact.
I'm also fine with not exposing this option to users.