k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

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

From: <daparpon AT dsic.upv.es>
To: k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] Calling SMT Solver from K specification
Date: Tue, 11 Apr 2017 04:01:23 -0500

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