K-user mailing list

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

Hi Daniel,

- You're right that (X):Sort restricts to X being of Sort and does not 
cast X to Sort.
Not sure then why the second solution works - without it the parser says 
that of the two rules it can apply it'll pick the one where the sort is 
K, while with it it goes for Bool instead. (it actually had the opposite 
effect with solution 1!)

So, no idea how to cast something with K. :-(

Looking at builtins/bool.k I can see an "andBool" and an "andThenBool", 
where the second uses K as one of its arguments - wonder whether that 
was introduced for a similar reason.

- For getModel I get the same errors as you do, depending on what I import.

I've tried to find where the two appear:
find .../k-3.6-2014-06-12/include -type f | xargs grep checkSat
find .../k-3.6-2014-06-12/include -type f | xargs grep getModel

getModel appears only in smt.k - when I changed the definition of 
checkSat in there to match that of getModel there was no effect from a 
normal checkSat (i.e., I got back "sat", without any models).

checkSat appears in fol.k, smt.k, symbolic-calculus.k, symbolic-k.k (all 
in include/builtins).

Interestingly, checkSat appears also in include/java/hooks.properties 
(org.kframework.backend.java.symbolic.UseSMT.checkSat).

Looking at that code in the current version (from git), there's just one 
checkSat method - there's no getModel Java method anywhere in there (see 
k/java-backend/src/main/java/org/kframework/backend/java/symbolic/UseSMT.java 
).
The code of the checkSat Java method actually calls Z3's getModel and 
returns the variable mappings - no idea how the results of that can be 
retrieved from K though, if that Java method is indeed what ends up 
getting called.

Sorry I cannot shed any more light on this - quite lost myself... :-(

On 01/06/2017 14:28, 
daparpon AT dsic.upv.es
 wrote:
> Hi Christos, and thanks! I think I have already figured it out, though. As you
> say, it works perfectly by dealing with Strings instead of SmtResponses, but
> it seems that this happens because the whole infrastructure to communicate
> with Z3 is built-in and compiled in the prelude, at least in K 3.4. Which
> means that it is not necessary to require nor import the file "smt.k" and the
> modules "SMT-HOOKS" or "SMT-SYNTAX-HOOKS". I tried it and performs as
> expected.
>
> However, you highlight an interesting issue in your Solution 2 (which I also
> found while transferring to my setting), regarding sorts. As far as I know,
> the subexpression (XXX):Sort is not a casting, but a restriction to the
> applicability of the rule; it means that the rule will only be applied if the
> restricted term (usually a variable) belongs to that sort. I do not know how
> to ask K for the actual sort of an expression, and it would be interesting to
> me, since my language does not call Z3 correctly because one of its arguments
> is not inferred to be Bool, although it should be. If anyone knows how to
> obtain or force the sort of an expression, can inform to us, please? It would
> be really appreciated.
>
> Finally, I add myself to the claim regarding getModel. In my case it is not
> just that getModel does not do anything, but I even get a syntax error while
> compiling:
>
> [Error] Critical: Parse error: Syntax error near unexpected character 'M'
>
> I have a hypothesis for this. In your case it may compile because your module
> imports "SMT-SYNTAX-HOOKS" in "smt.k", which declares both getModel and
> checkSat (the latter overloading the "checkSat(Bool) -> String" profile
> already defined), but gives no meaning to them. In my case I am purely relying
> on the infrastructure compiled in the prelude, and most likely getModel has
> not been defined there. There is indeed a rule for getModel in the "SMT-HOOKS"
> module, but trying to import it takes us back to square one, getting some
> syntax errors during compilation. Can you please try to import "SMT-HOOKS" and
> compile, to check whether it works for you or whether you get the same errors?
>
> Best regards,
> Daniel
>
> --------------------------------------------------------------------------------------------------
> 2017-05-31 19:26 GMT+03:00 <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