content: {-|
  Module      : What4.Solver
  Description : Reexports for working with solvers
  Copyright   : (c) Galois, Inc 2015-2020
  License     : BSD3
  Maintainer  : Rob Dockins <rdockins@galois.com>
  
  The module reexports the most commonly used types
  and operations for interacting with solvers.
  -}
  
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE OverloadedLists #-}
  
  module What4.Solver
    ( -- * Solver Adapters
      SolverAdapter(..)
    , ExprRangeBindings
    , defaultSolverAdapter
    , solverAdapterOptions
    , LogData(..)
    , logCallback
    , defaultLogData
    , smokeTest
    , module What4.SatResult
  
      -- * ABC (external, via SMT-Lib2)
    , ExternalABC(..)
    , externalABCAdapter
    , abcPath
    , abcOptions
    , runExternalABCInOverride
    , writeABCSMT2File
  
      -- * Bitwuzla
    , Bitwuzla(..)
    , bitwuzlaAdapter
    , bitwuzlaPath
    , bitwuzlaTimeout
    , runBitwuzlaInOverride
    , withBitwuzla
    , bitwuzlaOptions
    , bitwuzlaFeatures
  
      -- * Boolector
    , Boolector(..)
    , boolectorAdapter
    , boolectorPath
    , boolectorTimeout
    , runBoolectorInOverride
    , withBoolector
    , boolectorOptions
    , boolectorFeatures
  
      -- * CVC4
    , CVC4(..)
    , cvc4Adapter
    , cvc4Path
    , cvc4Timeout
    , runCVC4InOverride
    , writeCVC4SMT2File
    , withCVC4
    , cvc4Options
    , cvc4Features
  
      -- * CVC5
    , CVC5(..)
    , cvc5Adapter
    , cvc5Path
    , cvc5Timeout
    , runCVC5InOverride
    , writeCVC5SMT2File
    , withCVC5
    , cvc5Options
    , cvc5Features
  
      -- * DReal
    , DReal(..)
    , DRealBindings
    , drealAdapter
    , drealPath
    , runDRealInOverride
    , writeDRealSMT2File
  
      -- * STP
    , STP(..)
    , stpAdapter
    , stpPath
    , stpTimeout
    , runSTPInOverride
    , withSTP
    , stpOptions
    , stpFeatures
  
      -- * Yices
    , yicesAdapter
    , yicesPath
    , yicesEnableMCSat
    , yicesEnableInteractive
    , yicesGoalTimeout
    , runYicesInOverride
    , writeYicesFile
    , yicesOptions
    , yicesDefaultFeatures
  
      -- * Z3
    , Z3(..)
    , z3Path
    , z3Timeout
    , z3Tactic
    , z3TacticDefault
    , z3Adapter
    , runZ3InOverride
    , withZ3
    , z3Options
    , z3Features
    ) where
  
  import           What4.Solver.Adapter
  import           What4.Solver.Bitwuzla
  import           What4.Solver.Boolector
  import           What4.Solver.CVC4
  import           What4.Solver.CVC5
  import           What4.Solver.DReal
  import           What4.Solver.ExternalABC
  import           What4.Solver.STP
  import           What4.Solver.Yices
  import           What4.Solver.Z3
  import           What4.SatResult
  