k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[[K-user] ] SMT-based symbolic support in K 3.6

From: Camilo Rocha <camilo.rocha AT gmail.com>
To: k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] SMT-based symbolic support in K 3.6
Date: Thu, 15 Mar 2018 05:53:35 -0500
Authentication-results: illinois.edu; spf=pass smtp.mailfrom=camilo.rocha AT gmail.com; dkim=pass header.d=gmail.com header.s=20161025; dmarc=pass header.from=gmail.com

Dear K users,

We are trying to add symbolic support to a specification by using Boolean expressions (i.e., constraints) that can be queried for satisfiability with the help of an SMT-solver, such as the one integrated with K. In particular, we would like to treat symbolic constraints as a data type. We have been able to use the function

checkSat

available from

include/builtins/fol.k

to evaluate only *ground* constraints.

After following some of the threads in this list related to accessing SMT features from K specifications (e.g., https://lists.cs.illinois.edu/lists/arc/k-user/2017-06/msg00003.html) it is not clear whether this is possible.

I have the following specific questions:

0. Is it possible to treat Boolean constraints in K the way described above?

1. Is fol.k the right choice for this? In the above-mentioned thread, the file smt.k is mentioned, but it is not present in K 3.6.

2. How to build constraints with variables?

3. Do we need to upgrade to version 4 of K to deal with constraints as a data type and interact with the SMT solver?

Best regards,

Camilo Rocha

[[K-user] ] SMT-based symbolic support in K 3.6, Camilo Rocha, 03/15/2018