partial functions in symbolic rewriting

[daejunpark]

In java-backend's symbolic rewriting mode, if a condition of a rule contains a partial function which failed to evaluate, the rule is simply applied with a constraint having the unresolved function, which has little sense. We have two different situations in this regard:

• We may want to drop the current execution path entirely, especially for searching or proving. e.g., divide-by-zero
• We may want to consider those unresolved functions as bottom and the whole condition as false, especially for normal concrete execution. e.g., getKLabel applied to a token.

One possible solution would be to ask user to make every partial function as total, e.g., using [owise] rule. This will work for the second situation above, but may not for the first one. It would be better to discuss a general solution.

[bmmoore]

I agree paths should be dropped if the function is definitely stuck on (all ground instances of) the given arguments, but I think it makes plenty of sense to have unevaluated functions in side conditions in more general cases, if you consider such a constraint as also asserting that the function is actually defined on those arguments, and some way of checking whether a function is defined seems to be necessary for handling function applications with symbolic arguments (I suppose splitting states based on different clauses of a function definition might sometimes work, but it's not safe for recursive functions).

At the other side of tracking conditions in execution, we need to make sure that functions failing to evaluate is also considered wherever we need to calculate what conditions make a term stuck.

[daejunpark]

@cos could you take care of this? I think you can easily fix it at least for the case of KOOL: https://github.com/kframework/k/pull/1925/files#diff-577ed67708e4facf3a50380408fa9c30R949

[cos]

@daejunpark, [owise] can be easily handled by strategies. They are not active by default now, and it wouldn't be wise to activate them for the tutorial just now. Fixing this by other means would mean adding another special case in the backend, and I would rather avoid it. I'll mark this to be fixed later.