Enable using `cvc5` SMT solver in Kore

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework

BSD 3-Clause "New" or "Revised" License

212 stars 42 forks source link

Enable using `cvc5` SMT solver in Kore #3905

Open geo2a opened 6 months ago

geo2a commented 6 months ago

We have evidence (see Slack thread) that CVC5 is more successful than Z3 in dealing with some non-linear arithmetic problems arising in rules' side condition in kasmer and kontrol.

We have for a long time considered adding CVC5 as an alternative/companion solver to Z3.

We should start with the simplest possible implementation: use CVC5 instead of Z3, controlled by the --smt-solver command line option.

geo2a commented 6 months ago

@goodlyrottenapple experiment reveals that there are roadblocks in integrating CVC5 into Kore:

The smt-lemmas in evm-semantics use universal quntification to encode assumptions like forall X. 0 < keccak (X). While Z3 is happy with this, CVC5 does not support quantified assertions.
CVC5 has trouble consuming large SMT-LIB2 inputs, which are necessary to declare mutually-recursive assertions from Kore's SMT prelude. While there may be a way to restructure/rework the prelude so that the assertions are shorter, the input size constraint does not look promising.

More context could be found in this Slack thread. @goodlyrottenapple please add any other information you think is relevant.

goodlyrottenapple commented 6 months ago

The investigation also revealed that the way we encode data-types is similarly incompatible with CVC5; we are currently using forall quantifiers to send assertions such as no junk for each type. However, there is code which uses the standard declare-datatype smtlib functionality, which could be pulled out into a PR and merged as a stepping stone towards supporting other solvers (I have checked that using declare-datatype works in CVC5, however as mentioned before, CVC5 seems to break when the datatype declaration is too big)