Supporting multiple SMT solvers?

[ConnorBaker]

Hello!

Is supporting multiple SMT solvers a goal for this project?

I know that Liquid Haskell tries to do so, but (as far as I know) their CI doesn't test with anything other than Z3.

I tried to swap out Z3 for CVC5 via

--- a/src/Language/REST/SMT.hs
+++ b/src/Language/REST/SMT.hs
@@ -199,7 +199,7 @@ type SolverHandle = (Handle, Handle)
 
 spawnZ3 :: IO (Handle, Handle)
 spawnZ3 = do
-  (Just stdIn, Just stdOut, _, _) <- createProcess (proc "z3" ["-in"]) {std_in = CreatePipe, std_out = CreatePipe}
+  (Just stdIn, Just stdOut, _, _) <- createProcess (proc "cvc5" ["--incremental", "-"]) {std_in = CreatePipe, std_out = CreatePipe}
   return (stdIn, stdOut)

but ran into the following error when the test checking transitivity of KBO ran:

Exception: (error "Parse Error: <stdin>:325.73: 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)")

Curious if you have any thoughts or ideas!

[ConnorBaker]

@facundominguez any thoughts? Have you seen REST work with any solver besides Z3?

[facundominguez]

I would expect support for other smt solvers to be feasible, but I don't know which SMT solvers it is worth supporting. I have tried at some point LH with other smt solvers, but not rest-rewrite.