search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
444 stars 145 forks source link

Interface to call Z3 (or others) within K? #478

Closed LaifsV1 closed 3 years ago

LaifsV1 commented 5 years ago

Is there a way to call solvers for SMTLib formulas within K? Something with the intuition of the following rule:

rule <k> M => M' </k><pc> PC </pc> requires Sat(PC)

The idea is that a transition is taken only if the path condition PC is satisfiable.

dwightguth commented 5 years ago

Not currently, no.

nishantjr commented 5 years ago

I have worked on an interface for calling Z3 via the calls to #system. https://github.com/kframework/k/pull/350 I have not had the time to fix errors in the CI yet, though. @LaifsV1

LaifsV1 commented 5 years ago

@nishantjr what is the state of this? are there any working examples I could try?

nishantjr commented 5 years ago

There are examples in k-distribution/tests/regression-new/smtlib2/

run make after building K

nishantjr commented 5 years ago

Tests were passing locally on my machine, but not on the CI server. You need Z3/CVC4 in your system PATH

ehildenb commented 5 years ago

@nishantjr what's the status here?

nishantjr commented 5 years ago

We've got a working implementation being used for the matching logic prover. I have not had time to upstream it.

nishantjr commented 5 years ago

I'm not sure when I will be able to.

LaifsV1 commented 5 years ago

Is this done as a K module with system calls? Or does it use internal bindings (like the OCaml bindings for Z3)?

nishantjr commented 5 years ago

System calls still

ehildenb commented 3 years ago

This can be achieved using the system calls in K, and I think @nishantjr can post his example of the wrapper library he used for making this work here. Closing for now.