[smt-lemma] without [smtlib] must be disallowed

[denis-bogdanas]

To use [smt-lemma] on a rule, all functions used by the rule need some sort of smt translation, like [smt-lemma]. Thus cases like this must be rejected:

syntax Int ::= foo( Int )       [function]
rule foo(_) <Int 2 => true      [simplification, smt-lemma]

Currently compilation passes and in kprove [smt-lemma] is effectively ignored. This leads to hard to detect and time consuming bugs.

Full test: https://github.com/kframework/k/pull/1363 Version with [smtlib] that passes in Haskell: https://github.com/kframework/k/pull/1362

Full test, to put in regression-new/checks/smtLemmaNoSmtlib.k :

module SMTLEMMANOSMTLIB
    imports DOMAINS

    configuration <k> $PGM:Pgm </k>

    syntax Pgm ::= "ok"

    syntax Int ::= foo( Int )       [function]
    rule foo(I) => I %Int 2         [concrete]
    rule foo(_) <Int 2 => true      [simplification, smt-lemma]

endmodule

[dwightguth]

@ttuegel was there a reason you guys followed the Java backend behavior of dropping terms from the SMT that don't have smtlib attributes? is it possible this could be changed so that an smtlib symbol name is automatically generated from the kore symbol name? or would that break something in the backend? I'm hesitant to add a restriction here without first exploring whether or not there is a more user friendly solution.

[daejunpark]

I think one of the main reasons of the java backend having the existing behavior is the lack of comprehensive encoding of multi-sorted functions. But if the haskell backend does not suffer from the same limitation, I think it is a good idea to have an implicit smtlib attribute for all function symbols (in the haskell backend). But then, we may have the compatibility issue later.

[denis-bogdanas]

I guess you mean for all functions required by [smt-lemma]. Otherwise terms translated to z3 might get too big.

[ttuegel]

I think it would not be much trouble to try declaring all function symbols for the solver. We already declare all constructors. This would increase the size of terms sent to the solver, but the total time spent in the solver is pretty small so we have some room to work with.

[ehildenb]

One thing to keep in mind is that if we send all functions to the solver, the smtlib attribute doesn't mean much of anything anymore, except for controlling the symbol name that is sent to the solver (which is useful for smt-prelude options).

We should wait on this for when more of KEVM is migrated to the Haskell backend, because it provides an extensive test-suite for smtlib/smt-hook/smt-lemma.

We could also agree on the encoding technique used to send the symbols to the solver, so that the smt-prelude reason becomes moot.

[radumereuta]

Fixed by: https://github.com/runtimeverification/k/pull/2248