Avoid unmapping integers in multiplications with TPTP output #36

New Issue

patrick · 2019-01-30T00:44:25+01:00

patrick commented

2019-01-30 00:44:25 +01:00

Currently, multiplications in TPTP are “corrected” by undoing the mapping of variables of all sorts to integers only. That’s because integers are multiplied by 2 in the mapping, and multiplication of an integer n represented as 2 × n with an integer m represented as 2 × m leads to 4 × n × m, while 2 × n × m is the result we need.

Right now, the result is just wrapped in an f__unmap_integer__ function call, but this should be replaced by something that only uses the f__map_integer__ function instead.

Currently, multiplications in TPTP are “corrected” by undoing the mapping of variables of all sorts to integers only. That’s because integers are multiplied by 2 in the mapping, and multiplication of an integer *n* represented as 2 × *n* with an integer *m* represented as 2 × *m* leads to 4 × *n* × *m*, while 2 × *n* × *m* is the result we need. Right now, the result is just wrapped in an `f__unmap_integer__` function call, but this should be replaced by something that only uses the `f__map_integer__` function instead.

patrick added this to the anthem 0.2.0 milestone 2019-01-30 00:44:25 +01:00

patrick self-assigned this 2019-01-30 00:44:25 +01:00

patrick added the

enhancement

label 2019-01-30 00:44:25 +01:00

patrick closed this issue

2020-02-24 18:34:31 +01:00

Sign in to join this conversation.