K-user mailing list

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

I believe that K finds the rules in the SMT-HOOKS but the other rules imported from K builtins apply first  and reduce the _expression_ "4 >Int 4" before sending it to the solver. 

Can you try to use a symbolic value instead of 4?

Andrei

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

Yes, it does, but then functions and non-terminals from SMT-HOOKS such as
"checkSat" stop working. For instance, kompiling and krunning the same example
K spec as before...

require "builtins/smt.k"

module TEMP
imports SMT-SYNTAX-HOOKS

  syntax String ::= SMTR2String(SmtResponse)

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

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

endmodule

... results in the following output:

wifialu34-51:SMT Test ELP$ krun
<k>
    SMTR2String ( checkSat ( false ) )
</k>

To test further cases, I tried making "SMTR2String" a [strict] construction,
and then I got the following result:

wifialu34-51:SMT Test ELP$ krun
<k>
    checkSat ( false ) ~> SMTR2String ( HOLE )
</k>

So it seems that the execution gets stuck because K cannot find any rules that
give semantics to "checkSat", which are in the file SMT-HOOKS...

--------------------------------------------------------------------------------------------------
2017-05-15 07:57 GMT+03:00 <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