yav/simple-smt

simple-smt's Issues

need a reliable way to kill a solver process

I am starting two solvers concurrently. When one returns with a result, I want to kill the other. Ideally, the following should work

main = do
  as <- mapM async 
    [ main_with "yices-smt2" [ "--smt2-model-format" ]
    , main_with "cvc5" []
    ]
  (a,r) <- waitAnyCancel as
  print r

main_with :: String ->  [String] -> IO [(SExpr,Value)]
main_with solver opts = do
     l <- newLogger 0
     s <- newSolver solver opts (Just l)
     ...
     print =<< check s
     getExprs s [a,b,c,d]

but it does not. yices finds a solution, the program stops, but cvc5 keeps running.

output format of negative Reals not accepted by cvc5

I have this constraint

     x <- declare s "x" tReal
     assert s (mul (real 3) (add x (real 2)) `eq` real (negate 5))

communicating with cvc5 gives

[send->] (assert (= (* 3.0 (+ x 2.0)) -5.0))
[<-recv] (error "Parse Error: <stdin>:4.33: Symbol -5.0 is not declared. (assert (= (* 3.0 (+ x 2.0)) -5.0)) ^ ")
ex3: user error (Unexpected result from the SMT solver:
  Expected: success
  Result: (error "Parse Error: <stdin>:4.33: Symbol -5.0 is not declared. (assert (= (* 3.0 (+ x 2.0)) -5.0)) ^ ")
)

I guess they want (- 5.0) instead of -5.0.

yices-smt2 sometimes returns real value without decimal point

well, it's an edge case, but here goes:

[send->] (get-value (v15))
[<-recv] ((v15 0.0))    -- fine, has decimal point

[send->] (get-value (0.0))
[<-recv] ((0.0 0))       -- not fine

this sometimes happens in my application (some expressions might have been simplified but I do not keep track of it)

cvc5 sends back 0.0.

It's a bit hard to fix in simple-smt, since getExprs is not typed. I can fix it in my application https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/commit/a9dd4017030d7992132de745708ebfb2cabd51fb because I have typed expressions there.

define and use application-specific exceptions, instead of `fail`

(I was originally typing this as a comment on #13 but it's really about getResponse)

When I terminate a running solver, I am seeing "Missing response from solver" errors frequently - in the thread that's blocked on getResponse.

Well, that's life (there is no value that getResponse could return) but perhaps life can be made easier by using a different exception - instead of plain fail (from instance MonadFail IO, so it's failIO and it raises mkUserError _)

In my application code, I'd like to ignore that specific exception, but I want to see all others (because they might indicate problems).

addMany should have special case for one argument

With cvc5, I get this

[send->] (assert (<= (- 1.0) (+ (* (- 1.0) x0))))
[<-recv] (error "Parse Error: <stdin>:85.38: Invalid kind 'ADD', expected Terms with kind ADD must have at least 2 children and at most 67108863 children (the one under construction has 1) ")

sexprToVal fails for some Real representations

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)
21571e9

examples/ex1: Couldn't match expected type: IO Logger ...

ghc  examples/ex1.hs SimpleSMT.hs
...
examples/ex1.hs:5:11: error:
    • Couldn't match expected type: IO Logger
                  with actual type: Int -> IO Logger
    • Probable cause: ‘newLogger’ is applied to too few arguments
      In a stmt of a 'do' block: l <- newLogger

I think newLogger was extended with an argument, but the example was not updated.

The trivial fix is

 main =
-  do l <- newLogger
+  do l <- newLogger 0
      s <- newSolver "cvc4" ["--lang=smt2"] (Just l)

I can do it. Perhaps it should be part of a test suite. But this would probably require that some SMT solver is present. cvc4 is superseeded by cvc5, and for that, we can simply write

     s <- newSolver "cvc5" [] (Just l)

(we don't need the option).

adding solvers which provide bindings to parse SMTLib2

In Z3's API there is a function Z3_eval_smtlib2_string which can be used to interact with Z3 using SMTLib2 commands. Using such a binding is noticeably faster than launching Z3 as an external process and communicating with it through pipes.

I'm thus considering extending simple-smt to support using specific solvers that have this kind of bindings in their API. I'm thinking of something like having a

class Solver a where
  init :: IO a
  command :: a -> SExpr -> IO SExpr
  stop :: a -> IO ExitCode

with a generic instance Solver ExternalProcess for running solvers as external processes and then some more specific ones such as instance Solver Z3 for using solvers through their SMTLib2-parsing bindings.

If I were to make such a PR here, would it be accepted and actively maintained in the future ? Or I am better off forking this project ?

provide a Logger that writes to stderr

I propose to

newLogger :: Int -> IO Logger    -- keep the type
newLogger = newLoggerH stdout  -- refactor implementation

newLoggerH :: Handle -> Int -> IO Logger -- new function
newLoggerH h l = -- old implementation, with stdout replaced by h
  do tab <- newIORef 0
  ...