k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

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

From: "Zhang, Yi" <yzhng173 AT illinois.edu>
To: "daparpon AT dsic.upv.es" <daparpon AT dsic.upv.es>, "k-user AT lists.cs.illinois.edu" <k-user AT lists.cs.illinois.edu>
Subject: RE: [[K-user] ] Calling SMT Solver from K specification
Date: Tue, 11 Apr 2017 16:16:05 +0000
Accept-language: en-US

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

[[K-user] ] Calling SMT Solver from K specification, daparpon, 04/11/2017
- RE: [[K-user] ] Calling SMT Solver from K specification, Zhang, Yi, 04/11/2017
  - Re: [[K-user] ] Calling SMT Solver from K specification, daparpon, 04/12/2017
    - Message not available
      - [[K-user] ] Fwd: Calling SMT Solver from K specification, Andrei Arusoaie, 04/12/2017
        
        Re: [[K-user] ] Fwd: Calling SMT Solver from K specification, daparpon, 04/28/2017
        
        Re: [[K-user] ] Fwd: Calling SMT Solver from K specification, Andrei Arusoaie, 04/28/2017
        
        Re: [[K-user] ] Fwd: Calling SMT Solver from K specification, daparpon, 04/28/2017