1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Provers.Z3
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- The connection to the MathSAT SMT solver
-----------------------------------------------------------------------------
{-# LANGUAGE ScopedTypeVariables #-}
{-# 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
, supportsUninterpretedSorts = True
, supportsUnboundedInts = True
, supportsInt2bv = True
, supportsReals = True
, supportsApproxReals = True
, supportsDeltaSat = Nothing
, supportsIEEE754 = True
, supportsSets = True
, supportsOptimization = True
, supportsPseudoBooleans = True
, supportsCustomQueries = True
, supportsGlobalDecls = True
, supportsDataTypes = True
, supportsFoldAndMap = True
, supportsSpecialRels = True
, supportsDirectAccessors = 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
|
