Z3.hs

-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Provers.Z3
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- The connection to the Z3 SMT solver
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Provers.Z3(z3) where

import Data.SBV.Core.Data
import Data.SBV.SMT.SMT

-- | The description of the Z3 SMT solver.
-- The default executable is @\"z3\"@, which must be in your path. You can use the @SBV_Z3@ environment variable to point to the executable on your system.
-- You can use the @SBV_Z3_OPTIONS@ environment variable to override the options.
z3 :: SMTSolver
z3 = SMTSolver {
           name         = Z3
         , executable   = "z3"
         , preprocess   = id
         , options      = modConfig ["-nw", "-in", "-smt2"]
         , engine       = standardEngine "SBV_Z3" "SBV_Z3_OPTIONS"
         , capabilities = SolverCapabilities {
                                supportsQuantifiers     = True
                              , supportsDefineFun       = True
                              , supportsDistinct        = True
                              , supportsBitVectors      = True
                              , supportsADTs            = True
                              , supportsUnboundedInts   = True
                              , supportsReals           = True
                              , supportsApproxReals     = True
                              , supportsDeltaSat        = Nothing
                              , supportsIEEE754         = True
                              , supportsSets            = True
                              , supportsOptimization    = True
                              , supportsPseudoBooleans  = True
                              , supportsCustomQueries   = True
                              , supportsGlobalDecls     = True
                              , supportsDataTypes       = True
                              , supportsLambdas         = True
                              , supportsSpecialRels     = True
                              , supportsDirectTesters   = False -- Needs ascriptions. (See the CVC4 version of this)
                              , supportsFlattenedModels = Just [ "(set-option :pp.max_depth      4294967295)"
                                                               , "(set-option :pp.min_alias_size 4294967295)"
                                                               , "(set-option :model.inline_def  true      )"
                                                               ]
                              }
         }

 where modConfig :: [String] -> SMTConfig -> [String]
       modConfig opts _cfg = opts