/
ABC.hs
52 lines (48 loc) · 2.45 KB
/
ABC.hs
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
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Provers.ABC
-- Copyright : (c) Adam Foltzer
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- The connection to the ABC verification and synthesis tool
-----------------------------------------------------------------------------
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Provers.ABC(abc) where
import Data.SBV.Core.Data
import Data.SBV.SMT.SMT
-- | The description of abc. The default executable is @\"abc\"@,
-- which must be in your path. You can use the @SBV_ABC@ environment
-- variable to point to the executable on your system. The default
-- options are @-S \"%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000\"@.
-- You can use the @SBV_ABC_OPTIONS@ environment variable to override the options.
abc :: SMTSolver
abc = SMTSolver {
name = ABC
, executable = "abc"
, preprocess = id
, options = const ["-S", "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"]
, engine = standardEngine "SBV_ABC" "SBV_ABC_OPTIONS"
, capabilities = SolverCapabilities {
supportsQuantifiers = False
, supportsDefineFun = True
, supportsDistinct = True
, supportsBitVectors = True
, supportsUninterpretedSorts = False
, supportsUnboundedInts = False
, supportsInt2bv = False
, supportsReals = False
, supportsApproxReals = False
, supportsDeltaSat = Nothing
, supportsIEEE754 = False
, supportsSets = False
, supportsOptimization = False
, supportsPseudoBooleans = False
, supportsCustomQueries = False
, supportsGlobalDecls = False
, supportsDataTypes = False
, supportsDirectAccessors = False
, supportsFlattenedModels = Nothing
}
}