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

{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Provers.CVC4(cvc4) where

import Data.Char (isSpace)

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

-- | The description of the CVC4 SMT solver
-- The default executable is @\"cvc4\"@, which must be in your path. You can use the @SBV_CVC4@ environment variable to point to the executable on your system.
-- The default options are @\"--lang smt\"@. You can use the @SBV_CVC4_OPTIONS@ environment variable to override the options.
cvc4 :: SMTSolver
cvc4 :: SMTSolver
cvc4 = SMTSolver :: Solver
-> String
-> (String -> String)
-> (SMTConfig -> [String])
-> SMTEngine
-> SolverCapabilities
-> SMTSolver
SMTSolver {
           name :: Solver
name         = Solver
CVC4
         , executable :: String
executable   = String
"cvc4"
         , preprocess :: String -> String
preprocess   = String -> String
clean
         , options :: SMTConfig -> [String]
options      = [String] -> SMTConfig -> [String]
forall a b. a -> b -> a
const [String
"--lang", String
"smt", String
"--incremental", String
"--interactive", String
"--no-interactive-prompt", String
"--model-witness-value"]
         , engine :: SMTEngine
engine       = String -> String -> SMTEngine
standardEngine String
"SBV_CVC4" String
"SBV_CVC4_OPTIONS"
         , capabilities :: SolverCapabilities
capabilities = SolverCapabilities :: Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Maybe String
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Maybe [String]
-> SolverCapabilities
SolverCapabilities {
                                supportsQuantifiers :: Bool
supportsQuantifiers        = Bool
True
                              , supportsDefineFun :: Bool
supportsDefineFun          = Bool
True
                              , supportsDistinct :: Bool
supportsDistinct           = Bool
True
                              , supportsBitVectors :: Bool
supportsBitVectors         = Bool
True
                              , supportsUninterpretedSorts :: Bool
supportsUninterpretedSorts = Bool
True
                              , supportsUnboundedInts :: Bool
supportsUnboundedInts      = Bool
True
                              , supportsInt2bv :: Bool
supportsInt2bv             = Bool
True
                              , supportsReals :: Bool
supportsReals              = Bool
True  -- Not quite the same capability as Z3; but works more or less..
                              , supportsApproxReals :: Bool
supportsApproxReals        = Bool
False
                              , supportsDeltaSat :: Maybe String
supportsDeltaSat           = Maybe String
forall a. Maybe a
Nothing
                              , supportsIEEE754 :: Bool
supportsIEEE754            = Bool
True
                              , supportsSets :: Bool
supportsSets               = Bool
False
                              , supportsOptimization :: Bool
supportsOptimization       = Bool
False
                              , supportsPseudoBooleans :: Bool
supportsPseudoBooleans     = Bool
False
                              , supportsCustomQueries :: Bool
supportsCustomQueries      = Bool
True
                              , supportsGlobalDecls :: Bool
supportsGlobalDecls        = Bool
True
                              , supportsDataTypes :: Bool
supportsDataTypes          = Bool
True
                              , supportsDirectAccessors :: Bool
supportsDirectAccessors    = Bool
True
                              , supportsFlattenedModels :: Maybe [String]
supportsFlattenedModels    = Maybe [String]
forall a. Maybe a
Nothing
                              }
         }
  where -- CVC4 wants all input on one line
        clean :: String -> String
clean = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
simpleSpace (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
noComment

        noComment :: String -> String
noComment String
""       = String
""
        noComment (Char
';':String
cs) = String -> String
noComment (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'\n') String
cs
        noComment (Char
c:String
cs)   = Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
noComment String
cs

        simpleSpace :: Char -> Char
simpleSpace Char
c
          | Char -> Bool
isSpace Char
c = Char
' '
          | Bool
True      = Char
c