K-user mailing list

[Christos Kloukinas <c.kloukinas AT gmail.com>]

Hi, here are two ways I managed to get it to work (at least what I 
_think_ you were trying to achieve).
I think the problem has something to do with sorts (I'm total new to K, 
so I'm not very sure of what's going on).
I also think that you should avoid SmtResponse and use String directly.

- Solution 1:

module TEMP
imports SMT-SYNTAX-HOOKS
syntax String ::= "SMTR2String" "(" String ")" // [function]
rule SMTR2String("sat") => "SATISFIABLE" [structural]
rule SMTR2String("unsat") => "NOT SATISFIABLE" [structural]
configuration <k> SMTR2String(checkSat(#symInt(1) >Int #symInt(2))) </k>
endmodule

- Solution 2:

module TEMP
imports SMT-SYNTAX-HOOKS
// configuration <k> checkSat(notBool(notBool(#symInt(1) >Int 
#symInt(2)))) </k> // alternative configuration
configuration <k> checkSat((#symInt(1) >Int #symInt(2)):Bool) </k>  // 
Is (XXX):Bool casting XXX as Bool? Not sure...
rule "sat" => "SATISFIABLE"
rule "unsat" => "NOT SATISFIABLE"
endmodule


Now, if someone knows how to get a model out from the SMT solver, that'd 
be great!
I've tried to use getModel instead of checkSat but it doesn't seem to be 
doing anything:

require "builtins/smt.k"
module TEMP-MODEL
 imports SMT-SYNTAX-HOOKS
// configuration <k> checkSat( 10 <=Int #symInt(1) andBool #symInt(1) 
<=Int 12 ) </k> // reduces to "sat"
configuration <k> getModel( 10 <=Int #symInt(1) andBool #symInt(1) <=Int 
12 ) </k>
endmodule

Best,
Christos

On 15/05/2017 11:53, 
daparpon AT dsic.upv.es
 wrote:
> I tried, but the result remains the same:
>
> 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(#symInt(1) >Int #symInt(2))) </k>
>
> endmodule
>
> wifialu34-51:SMT Test ELP$ kompile temp.k --backend symbolic
> wifialu34-51:SMT Test ELP$ krun -cPC=true --search
> Search results:
>
> Solution 1:
> <k>
>      SMTR2String ( checkSat ( #symInt(1) >Int #symInt(2) ) )
> </k>
> <path-condition>
>      true
> </path-condition>
>
> Daniel
>
> --------------------------------------------------------------------------------------------------
> 2017-05-15 11:09 GMT+03:00 <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