Introducing Ordinal KORE Attribute

[Robertorosmaninho]

Closes https://github.com/Pi-Squared-Inc/pi2/issues/1432
This PR introduces a new attribute specific to the LLVM Backend. It includes the ordinal attribute to the KORE definition when preprocess is called after parsing a definition. The content of the attribute is a string_sort with the value of the computed axiom_ordinal.

A new C++ tool is planned to consume this feature instead of reading a definition with a bash script.
The main intention of this feature is to expose this information to the Python bindings to be used in Proof Hints integration tests.

[dwightguth]

this looks okay but I would want to make sure we've tested that the resulting attribute can be successfully grabbed by the python code that is consuming this before we merge this.

[Robertorosmaninho]

@dwightguth, I added some Python tests that use the new ordinal attribute.

• Some things to consider about this approach with Ordinal Attributes:

  • A downside of this approach is to perform a string comparison.
  • The upside is that we don't have to modify any K definitions to make that work.

• The other approach doesn't actually need the ordinal attribute; instead, we would need to create a new map <rule_label, axiom> and a function get_axiom_from_rule_label to avoid a linear search on the axioms every time we want to find a rule.

  • The downsides of this approach are that we must carry a new Map in every kore_definition, modify K definitions, and enforce that all rules we want to test must have a rule label.
  • The upside is that we can compare the ordinals instead of comparing strings.

[Baltoli]

I think the ordinal attribute approach is fine; this is ultimately testing infrastructure and so the performance of a string comparison isn't critical. Avoiding modifications of the K source code is nice.

[Baltoli]

One small change; otherwise good - feel free to merge once you've addressed it.