Add bdd_replace for monotonic renamings

[SSoelvsten]

As an initial step from the nested sweeping in v2.0 for the multi-variable quantification and the relational product in v2.1, we should address the basics of relabelling (assuming the relabelling function is monotonic).

• enum class replace_type: We need the user to differentiate between the following classes of renamings (enum values):

  • non-monotonic: This type of relabelling is left for the v2.2 milestone, since it requires moving the levels around.
  • monotonic: This type of relabelling encompasses all relabellings actively used in a model checker. Yet, we can look at the following restrictions
    • affine: Any relabelling of the form ax + b where a is a fraction (where ax is still an integer) and b is an integer.
    • shift: Any relabelling of the form x+b where b is an integer.

• Multi-call Mapping (bdd): functions with the following interface

  /// Replacement of a normal BDD where the `replace_type` is determined automatically
  bdd bdd_replace(const bdd& f, const function<bdd::label_type(bdd::label_type)> &m);
  
  /// Replacement of a normal BDD where the user has specified what to expect from `m`
  bdd bdd_replace(const bdd& f, const function<bdd::label_type(bdd::label_type)> &m, replace_type m);

  • Throw an error if m is non-monotonic. This other case is left for the v2.2 milestone.
  • Add helper functions for relabelling ptr, node and level_info.
  • Create a copy of f with the node file and the level_info_file properly replaced.

• Multi-call Mapping (__bdd): functions with the following interface

  /// Replacement of a normal BDD where the `replace_type` is determined automatically
  bdd bdd_replace(__bdd&& f, const function<bdd::label_type(bdd::label_type)> &m);
  
  /// Replacement of a normal BDD where the user has specified what to expect from `m`
  bdd bdd_replace(__bdd&& f, const function<bdd::label_type(bdd::label_type)> &m, replace_type m);

  • Throw an error if m is non-monotonic. This other case is left for the v2.2 milestone.
  • Extend reduce to take a (monotonic) variable renaming.

• Single-call Mapping (bdd/__bdd): functions with the following interface:

  /// Generator over tuples of *(before, after)* in descending order on *before*. Any variable
  /// not mentioned is left as-is.
  bdd bdd_replace(const bdd& f, const generator<pair<bdd::label_type, bdd::label_type>> &m, replace_type m);
  
  /// Iterator version
  bdd bdd_replace(const bdd& f, ForwardIt begin, ForwardIt end, replace_type m);

  • Also incorporate this read-once into the reduce algorithm. To this end, the bdd is initially transposed.

• Affine Renaming (bdd): In this case, the relabelling can (similar to negation) be postponed until it is read later.

  • Extend the dd class with two variables, affine_mult (double) and affine_add (int).
  • Add helper function to affine_relabel ptr, node and level_info.
  • Add affine_relabel on-the-fly to the node_stream class.

• Shift Renaming (bdd): In this case, the relabelling can also be postponed. One can do so much cheaper than the affine renaming (in terms of CPU instructions). The approach is the same as the one above.

[SSoelvsten]

I have now resolved the most important parts of this issue. The rest (affine/shift renaming and read-once inputs) are left as nice-to-haves that can be given to a student programmer or volunteer.