Fixed regressions in TPTP back-end ppTransTPTP [#69689,#69690]

CLEARSY / pptranspog

Encoding of proof obligations generated by Atelier B to typed first-order formats (SMT, TPTP) using the ppTrans approach

GNU General Public License v3.0

0 stars 2 forks source link

Closed dde-cls closed 1 month ago

dde-cls commented 1 month ago

In the TPTP back-end, the translator needs to know:

which global ids have been created and are used in the proof obligation for the current goal
the order the corresponding declations need to be issued.

The parameter to represent the global ids has been changed from a std::set to a custom data type composed of a std::set and a std::vector.