module Copilot.Verifier.Solver
  ( Solver(..)
  , solverAdapter
  ) where

import qualified What4.Solver.Adapter as W4
import qualified What4.Solver.CVC4 as W4.CVC4
import qualified What4.Solver.CVC5 as W4.CVC5
import qualified What4.Solver.Yices as W4.Yices
import qualified What4.Solver.Z3 as W4.Z3

-- | General-purpose SMT solvers that @copilot-verifier@ supports.
data Solver
  = CVC4
  | CVC5
  | Yices
  | Z3
  deriving Int -> Solver -> ShowS
[Solver] -> ShowS
Solver -> String
(Int -> Solver -> ShowS)
-> (Solver -> String) -> ([Solver] -> ShowS) -> Show Solver
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Solver -> ShowS
showsPrec :: Int -> Solver -> ShowS
$cshow :: Solver -> String
show :: Solver -> String
$cshowList :: [Solver] -> ShowS
showList :: [Solver] -> ShowS
Show

-- | Return the @what4@ 'W4.SolverAdapter' corresponding to a given 'Solver'.
solverAdapter :: Solver -> W4.SolverAdapter st
solverAdapter :: forall (st :: * -> *). Solver -> SolverAdapter st
solverAdapter Solver
CVC4  = SolverAdapter st
forall (st :: * -> *). SolverAdapter st
W4.CVC4.cvc4Adapter
solverAdapter Solver
CVC5  = SolverAdapter st
forall (st :: * -> *). SolverAdapter st
W4.CVC5.cvc5Adapter
solverAdapter Solver
Yices = SolverAdapter st
forall (st :: * -> *). SolverAdapter st
W4.Yices.yicesAdapter
solverAdapter Solver
Z3    = SolverAdapter st
forall (st :: * -> *). SolverAdapter st
W4.Z3.z3Adapter