RuleSet names with more structure

[unp1]

Please describe your proposal in a ONE sentence

Allow rulesets (heuristics) to be defined with a list of additional arguments

Underlying problem

For several rulesets the strategies have to analyze the instantiation of the schema variables to correctly compute the costs.
At the moment the strategies assume fixed names of the schema variables if a taclet is equipped with a specific rule set. For example, the strategies require that a rule with the ruleset "cnf_andComm" has at least the schema variables "commLeft" and "commRight". It uses then the names to access the current instantiation and to compute an order to decide whether to commute them or not. This implicit relying on names is brittle.

You can find all instances of this problem by searching for the usage of instOf(...) in JavaDLStrategy.

Usage Scenario

Who (user scenario) would benefit from implementing the idea?

• Writers of taclets as easier reuse of existing strategy features is possible and better documented.
• Less likely to break proof search by accidently renaming schemavariables.

Describe a short use case scenario in which the suggested idea is featured.
Describe the solution you'd like: A clear and concise description of what you want to happen.

A suggestion would be to be able to declate rule sets as

<name>(<list of named parameters>)

For example,

eqSymm(left: commLeft, right: commRight)

and the to allow the strategies to access the SVs via the names (here: left, right) and or simply by ...get(0)

Alternatives

A clear and concise description of any alternative solutions or features you've considered.
Why is the suggestion the best alternative?

Ideally (not alone with that feature request as compilation of rule sets would be required), the consistency would be checkable at compile time.

Estimated effort

If you can: Estimate the effort that has to be invested to implement the feature request.
Is there still discussion needed? Or is it purely implementation? Expertises needed?

• Adaptation of parser: straight forward
• Extension of RuleSet record: simple (at least when not using named parameters, but simply the order)
• Making the parameters accessible to the strategy: medium (requires some decisions about how to provide efficient access, maybe slight extension of the rule class to access rulesets quicker by name than just iterating over all entries)
• Adapting the instOf(...) calls in JavaDLStrategy and updating the rule files: simple, but needs care

Additional context

Add any other context or screenshots about the feature request here.