K-user mailing list

[Andrei Arusoaie <andrei.arusoaie AT gmail.com>]

I've hit the wrong button, sorry. Here's my answer to Daniel.

Andrei A.

---------- Forwarded message ----------
From: Andrei Arusoaie <andrei.arusoaie AT gmail.com>
Date: 2017-04-12 19:47 GMT+03:00
Subject: Re: [[K-user] ] Calling SMT Solver from K specification
To: daparpon AT dsic.upv.es

Hi Daniel,

If you’re using K-3.4 then you can take a look at k/include/builtins/smt.k, specifically in module:

module SMT-SYNTAX-HOOKS

  syntax SmtResponse ::= "sat"
                       | "unsat"
               | "unknown"
               | "model" "(" Map ")"

  syntax SmtResponse ::= "checkSat" "(" K ")" [function]
                       | "getModel" "(" K ")" [function]

  syntax Bool ::= SmtResponse "=/=" SmtResponse
        | SmtResponse "==" SmtResponse
endmodule

I think checkSat is what you’re looking for. Make sure you pass a Bool to it. If you need more, you can extend the module to translate whatever exp to SMTLib as we implicitly did for ints and bools (check the entire smt.k file for details).

Andrei A.

​

2017-04-12 17:07 GMT+03:00 <daparpon AT dsic.upv.es>:

What I need to do is to compare two symbolic execution states, S1 and S2,
which respectively contain the path conditions PC1 and PC2. The comparison is
simply done by checking whether the implication PC1 => PC2 holds. For
instance, this is a valid implication, where each ?vi is a symbolic value

(?v1 < ?v3 ^ ?v3 < ?v2) => (?v1 <= ?v2)

Since path conditions are logical expressions involving symbolic data, the
implication cannot be solved by means of K's boolean operators but I need to
delegate this problem to a SAT/SMT Solver.

How can I send the constraint to the SAT solver and get the solver verdict in
return?

I am still using K 3.4 since I need to read the path-condition cell during
symbolic execution, while K 4.0 does not have this capability available yet.

Thanks a lot and sorry for the inconveniencies. Best regards,
Daniel
________________________________________
From:
yzhng173 AT illinois.edu

[yzhng173 AT illinois.edu]
Sent: Tuesday, April 11, 2017 9:16 AM
To:
k-user AT lists.cs.illinois.edu
Subject: RE: [[K-user] ] Calling SMT Solver from K specification

Hi Daniel,

The current Java backend is using Z3 in the symbolic execution engine
internally and it is not exposed to the user. Could you please tell us more
specifically about your use cases?

Best,

Yi
________________________________________
From:
daparpon AT dsic.upv.es

[daparpon AT dsic.upv.es]
Sent: Tuesday, April 11, 2017 4:01 AM
To:
k-user AT lists.cs.illinois.edu

Subject: [[K-user] ] Calling SMT Solver from K specification

Hi! I am implementing a part of my K language specification which needs to
check a boolean formula for satisfiability/validity. How can I do that in K?
Are there any built-in commands or terms that allow K rules to communicate
with an SMT Solver, for instance Z3? In that case, which are they (or where
can I find more information about them)?

Thanks in advance,
Daniel