Encoding symbolic and concrete in Kore

[ana-pantilie]

K currently allows users to mark function definition rules as symbolic or concrete. Since function definitions have semantic value, the symbolic and concrete attribute need to have an encoding in Kore/ML. We need to figure out if our main semantics use this feature, and if they do, to figure out if such an encoding exists.

Note: this is for function definition rules not simplification rules

Related #3385

[ehildenb]

concrete is only used on some function rules in KEVM, and there we do actually use it. The one restriction that is (loosely) enforced is that all the rules for that production must be marked as concrete, which I think is sufficient to allow us to not make an ML encoding for it. So instead, I would suggest:

• concrete and symbolic can only show up on simplification rules.
• concrete can show up on function productions, and it means that all the equational axioms for the function symboll are concrete. This should allow us to avoid encoding concrete to ML, because we can either take all or none o the equational axioms based on the term we're inspecting.

These should be enforced by the frontend.

[ehildenb]

Will have to update KEVM to do this.