search

yav / simple-smt

BSD 3-Clause "New" or "Revised" License
20 stars 20 forks source link

sexprToVal fails for some Real representations #16

Open jwaldmann opened 2 years ago

jwaldmann commented 2 years ago

current implementation has just one branch that builds a Real

sexprToVal :: SExpr -> Value
sexprToVal expr =
  case expr of
...
    List [ Atom "/", x, y ]
      | Int a <- sexprToVal x
      , Int b <- sexprToVal y    -> Real (a % b)

but solvers also produce other forms: z3 sends

[send->] (get-value (x0))
[<-recv] ((x0 (- (/ 1.0 18000.0))))
[send->] (get-value (x1))
[<-recv] ((x1 0.0))

I added a test case (in my fork) https://github.com/yav/simple-smt/commit/21571e9aa628c70552705610cde56fe21bb04c0a

jwaldmann commented 2 years ago

with previous commit, I can parse output from "z3" [ "-in", "-smt2" ]

yav commented 2 years ago

Thanks for reporting this. Unfortunately the output formats for the various solvers are not very well documented. Please make a PR, would be happy to merge.

jwaldmann commented 2 years ago

No, output format is well-defined (meanwhile)? See 4.2.6 "Inspecting models" of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf

Yes, I will send PR.