K-user mailing list

[<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