K-user mailing list

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

I think you should import SMT-SYTNAX-HOOKS. Does it compile?

Andrei

2017-05-12 11:39 GMT+03:00 <daparpon AT dsic.upv.es>:

Thanks! I tried your example and works for me as well. However, it seems that
the problem arises when explicitly manipulating elements of sort SmtResponse.
For instance, I modified the example introducing a function that takes a
SmtResponse parameter, and now I get an error saying that the SmtResponse sort
is undefined:

require "builtins/smt.k"

module TEMP

  syntax String ::= SMTR2String(SmtResponse)

  rule SMTR2String(sat) => "SATISFIABLE"                                                [structural]
  rule SMTR2String(unsat) => "NOT SATISFIABLE"                                  [structural]

  configuration <k> SMTR2String(checkSat(4 >Int 4)) </k>

endmodule

wifialu32-238:SMT Test ELP$ kompile temp.k
[Error] Compiler: Undefined sort SmtResponse
        File: /Users/ELP/Desktop/KTests/SMT Test/temp.k
        Location: (5,33,5,43)
        Compilation Phase: class org.kframework.compile.checks.CheckSyntaxDecl

I tried to solve it by adding "imports SMT-HOOKS" below the "module TEMP"
declaration, but then the error that I reported in previous messages returned:

wifialu32-238:SMT Test ELP$ kompile temp.k
[Warning] Compiler: Associativity attribute should only be assigned to binary
infix production.

        File: /Users/ELP/Documents/k/include/builtins/fol.k
        Location: (14,18,14,57)
        Compilation Phase: class org.kframework.compile.checks.CheckSyntaxDecl
[Warning] Compiler: Associativity attribute should only be assigned to binary
infix production.

        File: /Users/ELP/Documents/k/include/builtins/fol.k
        Location: (15,18,15,57)
        Compilation Phase: class org.kframework.compile.checks.CheckSyntaxDecl
[Error] Critical: Parse error: Syntax error near unexpected character 'y'
        File: /Users/ELP/Documents/k/include/builtins/smt.k
        Location: (17,16,17,16)

Thanks again and sorry for the inconveniencies,
Daniel

--------------------------------------------------------------------------------------------------

2017-05-11 16:00 GMT+03:00 <andrei.arusoaie AT gmail.com>:

I’ve done the following experiment (please note the commented line no 4 in
smt.k) and it works for me:

[andrei]-$ cat /home/andrei/Downloads/k/include/builtins/smt.k
// Copyright (c) 2012-2014 K Team. All Rights Reserved.
require "builtins/builtins.k"
require "builtins/fol.k"
// require "builtins/array-symbolic.k"

module SMTLIB-CONVERSION
  imports BUILTIN-HOOKS
  imports FOL
  ...


[andrei]-$ cat temp.k
require "builtins/smt.k"

module TEMP

  configuration <k> checkSat(4 >Int 4) </k>

endmodule
[andrei]-$ ./kompile --version
K-framework version 3.4.
Git Revision: 08c9271
Build date: Tue Aug 26 13:56:56 PDT 2014

[andrei]-$ ./kompile temp.k

[andrei]-$ ./krun
<k>
    "unsat"
</k>

Andrei
​

2017-05-11 15:19 GMT+03:00 Andrei Arusoaie <andrei.arusoaie AT gmail.com>:

    Hi,

    Can you attach a simple K file which can reproduce the bug?
    Andrei

    2017-05-11 10:27 GMT+03:00 <daparpon AT dsic.upv.es>:

        Hi, Andrei.

        Please can you give me any recommendations regarding this problem?
Since I'm
        not able to make K interact with the SMT solver, I'm stuck in this
phase of my
        research.

        Thanks in advance,
        Daniel


--------------------------------------------------------------------------------------------------
        2017-04-28 13:25 GMT+03:00 <daparpon AT dsic.upv.es>:

        Nope, it does not. I tried commenting the "require array-symbolic.k"
clause
        and I obtained other kompiling errors and warnings, specifically the
following
        ones:

        [Warning] Compiler: Associativity attribute should only be assigned to
binary
        infix production.

        File: /Users/ELP/Documents/k/include/builtins/fol.k
        Location: (14,18,14,57)
        Compilation Phase: class org.kframework.compile.checks.CheckSyntaxDecl

        [Warning] Compiler: Associativity attribute should only be assigned to
binary
        infix production.

        File: /Users/ELP/Documents/k/include/builtins/fol.k
        Location: (15,18,15,57)
        Compilation Phase: class org.kframework.compile.checks.CheckSyntaxDecl

        [Error] Critical: Parse error: Syntax error near unexpected character
'y'
        File: /Users/ELP/Documents/k/include/builtins/smt.k
        Location: (17,16,17,16)

        To be more precise, the line which the error refers to is:

        rule Smtlib(symBool(I:Int)) => "var" +String Int2String(I)

        and the location reference points to the 'y' in "symBool(I:Int)".

        Daniel


--------------------------------------------------------------------------------------------------
        2017-04-28 13:16 GMT+03:00 <andrei.arusoaie AT gmail.com>:

        That's weird...
        Anyway, I think you can comment the line which include array-
symbolic.k from /
        k/include/builtins/smt.k.
        Does it work if you do that?


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

        Hi! I tried to import the module you refer to (and insert the proper "
        require
        "builtins/smt.k" " clause) in order to use the checkSat function in my
        language. However, when I kompile the resulting specification, I get
the
        following error message:

        [Error] Critical: Could not find 'required' file: builtins/array-
        symbolic.k
        File: <filepath to K>/k/include/builtins/smt.k
        Location: (4,1,4,35)

        I have looked for the "array-symbolic.k" file in both my file system
and
        previous distributions of the K Framework, but I could not find it
        anywhere.
        How can I solve this dependency and work with the "smt.k" file?

        Thanks in advance,
        Daniel

        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