Closed Robertorosmaninho closed 1 month ago
@dwightguth, I added some Python tests that use the new ordinal attribute.
Some things to consider about this approach with Ordinal Attributes:
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.
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.
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 whenpreprocess
is called after parsing a definition. The content of the attribute is astring_sort
with the value of the computedaxiom_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.