Add a transformation to make transition relation right-total

[Po-Chun-Chien]

This PR introduces a procedure that transforms a partial transition relation to a right-total one.

Some model-checking algorithms (such as the interpolation-based ones interp, ismc, and dar; recall #457) require the transition relation to be total.

For example, the invariant check for this Btor2 instance fails without the transformation:

$ ./pono --check-invar --bound 2000000000 --engine interp zipcpu-pfcache-p28.btor2
Invariant Check FAILED
terminate called after throwing an instance of 'PonoException'
  what():  Invariant Check FAILED
Aborted (core dumped)
$ ./pono --check-invar --ensure-trans-total --bound 2000000000 --engine interp zipcpu-pfcache-p28.btor2
Invariant Check PASSED
unsat
b0

Note that the auxiliary variable introduced by this transformation has to be removed from the invariant (cofactoring on valid = true) if we later want to export it as a correctness witness.

[Po-Chun-Chien]

The new transformation also has a surprising impact on solving performance.
When combined with the option --use-rel-ts introduced in #520 (see 6944d02), the engine ind can solve this Btor2 instance in about 330 seconds. Without the transformation, however, it fails to finish within 900 seconds.

$ ./pono --use-rel-ts --ensure-trans-total --bound 2000000000 --engine ind zipcpu-busdelay-p10.btor2 
unsat
b0
$ ./pono --bound 2000000000 --engine ind zipcpu-busdelay-p10.btor2 
# no answer after 900 s
$ ./pono --ensure-trans-total --bound 2000000000 --engine ind zipcpu-busdelay-p10.btor2
# no answer after 900 s