-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.SMT.SMTLib
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Conversion of symbolic programs to SMTLib format
-----------------------------------------------------------------------------

{-# LANGUAGE NamedFieldPuns #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.SMT.SMTLib (
          SMTLibPgm
        , toSMTLib
        , toIncSMTLib
        ) where

import qualified Data.Set as Set (member, toList)

import Data.SBV.Core.Data

import Data.SBV.SMT.Utils
import qualified Data.SBV.SMT.SMTLib2 as SMT2

-- | Convert to SMT-Lib, in a full program context.
toSMTLib :: SMTConfig -> SMTLibConverter SMTLibPgm
toSMTLib :: SMTConfig -> SMTLibConverter SMTLibPgm
toSMTLib SMTConfig{SMTLibVersion
smtLibVersion :: SMTConfig -> SMTLibVersion
smtLibVersion :: SMTLibVersion
smtLibVersion} = case SMTLibVersion
smtLibVersion of
                                      SMTLibVersion
SMTLib2 -> SMTLibConverter SMTLibPgm
toSMTLib2

-- | Convert to SMT-Lib, in an incremental query context.
toIncSMTLib :: SMTConfig -> SMTLibIncConverter [String]
toIncSMTLib :: SMTConfig -> SMTLibIncConverter [String]
toIncSMTLib SMTConfig{SMTLibVersion
smtLibVersion :: SMTLibVersion
smtLibVersion :: SMTConfig -> SMTLibVersion
smtLibVersion} = case SMTLibVersion
smtLibVersion of
                                         SMTLibVersion
SMTLib2 -> SMTLibIncConverter [String]
toIncSMTLib2

-- | Convert to SMTLib-2 format
toSMTLib2 :: SMTLibConverter SMTLibPgm
toSMTLib2 :: SMTLibConverter SMTLibPgm
toSMTLib2 = SMTLibVersion -> SMTLibConverter SMTLibPgm
cvt SMTLibVersion
SMTLib2
  where cvt :: SMTLibVersion -> SMTLibConverter SMTLibPgm
cvt SMTLibVersion
v QueryContext
ctx Set Kind
kindInfo Bool
isSat [String]
comments ([(Quantifier, NamedSymVar)], [NamedSymVar])
qinps [Either SV (SV, [SV])]
skolemMap (CnstMap, [(SV, CV)])
consts [((Int, Kind, Kind), [SV])]
tbls [(Int, ArrayInfo)]
arrs [(String, SBVType)]
uis [(String, [String])]
axs SBVPgm
asgnsSeq Seq (Bool, [(String, String)], SV)
cstrs SV
out SMTConfig
config
         | Kind
KUnbounded Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo Bool -> Bool -> Bool
&& Bool -> Bool
not (SolverCapabilities -> Bool
supportsUnboundedInts SolverCapabilities
solverCaps)
         = String -> SMTLibPgm
forall a. String -> a
unsupported String
"unbounded integers"
         | Kind
KReal Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo  Bool -> Bool -> Bool
&& Bool -> Bool
not (SolverCapabilities -> Bool
supportsReals SolverCapabilities
solverCaps)
         = String -> SMTLibPgm
forall a. String -> a
unsupported String
"algebraic reals"
         | (Bool
needsFloats Bool -> Bool -> Bool
|| Bool
needsDoubles) Bool -> Bool -> Bool
&& Bool -> Bool
not (SolverCapabilities -> Bool
supportsIEEE754 SolverCapabilities
solverCaps)
         = String -> SMTLibPgm
forall a. String -> a
unsupported String
"floating-point numbers"
         | Bool
needsQuantifiers Bool -> Bool -> Bool
&& Bool -> Bool
not (SolverCapabilities -> Bool
supportsQuantifiers SolverCapabilities
solverCaps)
         = String -> SMTLibPgm
forall a. String -> a
unsupported String
"quantifiers"
         | Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
sorts) Bool -> Bool -> Bool
&& Bool -> Bool
not (SolverCapabilities -> Bool
supportsUninterpretedSorts SolverCapabilities
solverCaps)
         = String -> SMTLibPgm
forall a. String -> a
unsupported String
"uninterpreted sorts"
         | Bool
True
         = SMTLibVersion -> [String] -> SMTLibPgm
SMTLibPgm SMTLibVersion
v [String]
pgm
         where sorts :: [String]
sorts = [String
s | KUserSort String
s Maybe [String]
_ <- Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
kindInfo]
               solverCaps :: SolverCapabilities
solverCaps = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
config)
               unsupported :: String -> a
unsupported String
w = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"SBV: Given problem needs " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w
                                               , String
"*** Which is not supported by SBV for the chosen solver: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
config))
                                               ]
               converter :: SMTLibConverter [String]
converter = case SMTLibVersion
v of
                             SMTLibVersion
SMTLib2 -> SMTLibConverter [String]
SMT2.cvt
               pgm :: [String]
pgm = SMTLibConverter [String]
converter QueryContext
ctx Set Kind
kindInfo Bool
isSat [String]
comments ([(Quantifier, NamedSymVar)], [NamedSymVar])
qinps [Either SV (SV, [SV])]
skolemMap (CnstMap, [(SV, CV)])
consts [((Int, Kind, Kind), [SV])]
tbls [(Int, ArrayInfo)]
arrs [(String, SBVType)]
uis [(String, [String])]
axs SBVPgm
asgnsSeq Seq (Bool, [(String, String)], SV)
cstrs SV
out SMTConfig
config

               needsFloats :: Bool
needsFloats  = Kind
KFloat  Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
               needsDoubles :: Bool
needsDoubles = Kind
KDouble Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
               needsQuantifiers :: Bool
needsQuantifiers
                 | Bool
isSat = Quantifier
ALL Quantifier -> [Quantifier] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Quantifier]
quantifiers
                 | Bool
True  = Quantifier
EX  Quantifier -> [Quantifier] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Quantifier]
quantifiers
                 where quantifiers :: [Quantifier]
quantifiers = ((Quantifier, NamedSymVar) -> Quantifier)
-> [(Quantifier, NamedSymVar)] -> [Quantifier]
forall a b. (a -> b) -> [a] -> [b]
map (Quantifier, NamedSymVar) -> Quantifier
forall a b. (a, b) -> a
fst (([(Quantifier, NamedSymVar)], [NamedSymVar])
-> [(Quantifier, NamedSymVar)]
forall a b. (a, b) -> a
fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
qinps)

-- | Convert to SMTLib-2 format
toIncSMTLib2 :: SMTLibIncConverter [String]
toIncSMTLib2 :: SMTLibIncConverter [String]
toIncSMTLib2 = SMTLibVersion -> SMTLibIncConverter [String]
cvt SMTLibVersion
SMTLib2
  where cvt :: SMTLibVersion -> SMTLibIncConverter [String]
cvt SMTLibVersion
SMTLib2 = SMTLibIncConverter [String]
SMT2.cvtInc