------------------------------------------------------------------------
-- |
-- Module           : What4.Protocol.SMTLib2
-- Description      : Interface for solvers that consume SMTLib2
-- Copyright        : (c) Galois, Inc 2014-2020
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
-- This module defines operations for producing SMTLib2-compatible
-- queries useful for interfacing with solvers that accecpt SMTLib2 as
-- an input language.
------------------------------------------------------------------------
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module What4.Protocol.SMTLib2
  ( -- SMTLib special purpose exports
    Writer
  , SMTLib2Tweaks(..)
  , newWriter
  , writeCheckSat
  , writeExit
  , writeGetValue
  , runCheckSat
  , asSMT2Type
  , setOption
  , getVersion
  , versionResult
  , getName
  , nameResult
  , setProduceModels
  , smtLibEvalFuns
    -- * Logic
  , SMT2.Logic(..)
  , SMT2.qf_bv
  , SMT2.allSupported
  , all_supported
  , setLogic
    -- * Type
  , SMT2.Sort(..)
  , SMT2.arraySort
    -- * Term
  , Term(..)
  , arrayConst
  , What4.Protocol.SMTLib2.arraySelect
  , arrayStore
    -- * Solvers and External interface
  , Session(..)
  , SMTLib2GenericSolver(..)
  , writeDefaultSMT2
  , startSolver
  , shutdownSolver
  , smtAckResult
  , SMTLib2Exception(..)
    -- * Solver version
  , ppSolverVersionCheckError
  , ppSolverVersionError
  , checkSolverVersion
  , checkSolverVersion'
  , queryErrorBehavior
  , defaultSolverBounds
    -- * Re-exports
  , SMTWriter.WriterConn
  , SMTWriter.assume
  , SMTWriter.supportedFeatures
  , SMTWriter.nullAcknowledgementAction
  ) where

#if !MIN_VERSION_base(4,13,0)
import Control.Monad.Fail( MonadFail )
#endif

import           Control.Applicative
import           Control.Exception
import           Control.Monad.State.Strict
import qualified Data.Attoparsec.Text as AT
import qualified Data.BitVector.Sized as BV
import qualified Data.Bits as Bits
import           Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import           Data.Char (digitToInt, isPrint, isAscii)
import           Data.IORef
import qualified Data.Text as Text
import qualified Data.Text.Lazy as Lazy
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Monoid
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.NatRepr
import           Data.Parameterized.Pair
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC
import           Data.Ratio
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.String
import           Data.Text (Text)
import           Data.Text.Lazy.Builder (Builder)
import qualified Data.Text.Lazy.Builder as Builder
import qualified Data.Text.Lazy.Builder.Int as Builder

import           Numeric (readDec, readHex, readInt, showHex)
import           Numeric.Natural
import qualified System.Exit as Exit
import qualified System.IO as IO
import qualified System.IO.Streams as Streams
import qualified System.IO.Streams.Attoparsec.Text as Streams
import           Data.Versions (Version(..))
import qualified Data.Versions as Versions
import qualified Prettyprinter as PP
import           LibBF( bfToBits )

import           Prelude hiding (writeFile)

import           What4.BaseTypes
import qualified What4.Expr.Builder as B
import           What4.Expr.GroundEval
import qualified What4.Interface as I
import           What4.ProblemFeatures
import           What4.Protocol.Online
import           What4.Protocol.ReadDecimal
import           What4.Protocol.SExp
import           What4.Protocol.SMTLib2.Syntax (Term, term_app, un_app, bin_app)

import qualified What4.Protocol.SMTLib2.Syntax as SMT2 hiding (Term)
import qualified What4.Protocol.SMTWriter as SMTWriter
import           What4.Protocol.SMTWriter hiding (assume, Term)
import           What4.SatResult
import           What4.Utils.FloatHelpers (fppOpts)
import           What4.Utils.HandleReader
import           What4.Utils.Process
import           What4.Utils.Versions
import           What4.Solver.Adapter

-- | Set the logic to all supported logics.
all_supported :: SMT2.Logic
all_supported :: Logic
all_supported = Logic
SMT2.allSupported
{-# DEPRECATED all_supported "Use allSupported" #-}

------------------------------------------------------------------------
-- Floating point

data SMTFloatPrecision =
  SMTFloatPrecision { SMTFloatPrecision -> Natural
smtFloatExponentBits :: !Natural
                      -- ^ Number of bits in exponent
                    , SMTFloatPrecision -> Natural
smtFloatSignificandBits :: !Natural
                      -- ^ Number of bits in the significand.
                    }
  deriving (SMTFloatPrecision -> SMTFloatPrecision -> Bool
(SMTFloatPrecision -> SMTFloatPrecision -> Bool)
-> (SMTFloatPrecision -> SMTFloatPrecision -> Bool)
-> Eq SMTFloatPrecision
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SMTFloatPrecision -> SMTFloatPrecision -> Bool
$c/= :: SMTFloatPrecision -> SMTFloatPrecision -> Bool
== :: SMTFloatPrecision -> SMTFloatPrecision -> Bool
$c== :: SMTFloatPrecision -> SMTFloatPrecision -> Bool
Eq, Eq SMTFloatPrecision
Eq SMTFloatPrecision
-> (SMTFloatPrecision -> SMTFloatPrecision -> Ordering)
-> (SMTFloatPrecision -> SMTFloatPrecision -> Bool)
-> (SMTFloatPrecision -> SMTFloatPrecision -> Bool)
-> (SMTFloatPrecision -> SMTFloatPrecision -> Bool)
-> (SMTFloatPrecision -> SMTFloatPrecision -> Bool)
-> (SMTFloatPrecision -> SMTFloatPrecision -> SMTFloatPrecision)
-> (SMTFloatPrecision -> SMTFloatPrecision -> SMTFloatPrecision)
-> Ord SMTFloatPrecision
SMTFloatPrecision -> SMTFloatPrecision -> Bool
SMTFloatPrecision -> SMTFloatPrecision -> Ordering
SMTFloatPrecision -> SMTFloatPrecision -> SMTFloatPrecision
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SMTFloatPrecision -> SMTFloatPrecision -> SMTFloatPrecision
$cmin :: SMTFloatPrecision -> SMTFloatPrecision -> SMTFloatPrecision
max :: SMTFloatPrecision -> SMTFloatPrecision -> SMTFloatPrecision
$cmax :: SMTFloatPrecision -> SMTFloatPrecision -> SMTFloatPrecision
>= :: SMTFloatPrecision -> SMTFloatPrecision -> Bool
$c>= :: SMTFloatPrecision -> SMTFloatPrecision -> Bool
> :: SMTFloatPrecision -> SMTFloatPrecision -> Bool
$c> :: SMTFloatPrecision -> SMTFloatPrecision -> Bool
<= :: SMTFloatPrecision -> SMTFloatPrecision -> Bool
$c<= :: SMTFloatPrecision -> SMTFloatPrecision -> Bool
< :: SMTFloatPrecision -> SMTFloatPrecision -> Bool
$c< :: SMTFloatPrecision -> SMTFloatPrecision -> Bool
compare :: SMTFloatPrecision -> SMTFloatPrecision -> Ordering
$ccompare :: SMTFloatPrecision -> SMTFloatPrecision -> Ordering
$cp1Ord :: Eq SMTFloatPrecision
Ord)

asSMTFloatPrecision :: FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision :: FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision (FloatingPointPrecisionRepr NatRepr eb
eb NatRepr sb
sb) =
  SMTFloatPrecision :: Natural -> Natural -> SMTFloatPrecision
SMTFloatPrecision { smtFloatExponentBits :: Natural
smtFloatExponentBits = NatRepr eb -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr eb
eb
                    , smtFloatSignificandBits :: Natural
smtFloatSignificandBits = NatRepr sb -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr sb
sb
                    }

mkFloatSymbol :: Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol :: Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
nm (SMTFloatPrecision Natural
eb Natural
sb) =
  Builder
"(_ "
    Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
nm
    Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" "
    Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. IsString a => String -> a
fromString (Natural -> String
forall a. Show a => a -> String
show Natural
eb)
    Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" "
    Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. IsString a => String -> a
fromString (Natural -> String
forall a. Show a => a -> String
show Natural
sb)
    Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

------------------------------------------------------------------------
-- SMTLib2Tweaks

-- | Select a valued from a nested array
nestedArrayUpdate :: Term
                  -> (Term, [Term])
                  -> Term
                  -> Term
nestedArrayUpdate :: Term -> (Term, [Term]) -> Term -> Term
nestedArrayUpdate Term
a (Term
h,[]) Term
v  = Term -> Term -> Term -> Term
SMT2.store Term
a Term
h Term
v
nestedArrayUpdate Term
a (Term
h,Term
i:[Term]
l) Term
v = Term -> Term -> Term -> Term
SMT2.store Term
a Term
h Term
sub_a'
  where sub_a' :: Term
sub_a' = Term -> (Term, [Term]) -> Term -> Term
nestedArrayUpdate (Term -> Term -> Term
SMT2.select Term
a Term
h) (Term
i,[Term]
l) Term
v

arrayConst :: SMT2.Sort -> SMT2.Sort -> Term -> Term
arrayConst :: Sort -> Sort -> Term -> Term
arrayConst = Sort -> Sort -> Term -> Term
SMT2.arrayConst

arraySelect :: Term -> Term -> Term
arraySelect :: Term -> Term -> Term
arraySelect = Term -> Term -> Term
SMT2.select

arrayStore :: Term -> Term -> Term -> Term
arrayStore :: Term -> Term -> Term -> Term
arrayStore = Term -> Term -> Term -> Term
SMT2.store

byteStringTerm :: ByteString -> Term
byteStringTerm :: ByteString -> Term
byteStringTerm ByteString
bs = Builder -> Term
SMT2.T (Builder
"\"" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (Word8 -> Builder -> Builder) -> Builder -> ByteString -> Builder
forall a. (Word8 -> a -> a) -> a -> ByteString -> a
BS.foldr Word8 -> Builder -> Builder
forall a. (Integral a, Show a, Bits a) => a -> Builder -> Builder
f Builder
"\"" ByteString
bs)
 where
 f :: a -> Builder -> Builder
f a
w Builder
x
   | Char
'\"' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c = Builder
"\"\"" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
x
   | Char -> Bool
isPrint Char
c = Char -> Builder
Builder.singleton Char
c Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
x
   | Bool
otherwise = Builder
"\\x" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
h1 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
h2  Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
x
  where
  h1 :: Builder
h1 = String -> Builder
Builder.fromString (a -> ShowS
forall a. (Integral a, Show a) => a -> ShowS
showHex (a
w a -> Int -> a
forall a. Bits a => a -> Int -> a
`Bits.shiftR` Int
4) String
"")
  h2 :: Builder
h2 = String -> Builder
Builder.fromString (a -> ShowS
forall a. (Integral a, Show a) => a -> ShowS
showHex (a
w a -> a -> a
forall a. Bits a => a -> a -> a
Bits..&. a
0xF) String
"")

  c :: Char
  c :: Char
c = Int -> Char
forall a. Enum a => Int -> a
toEnum (a -> Int
forall a. Enum a => a -> Int
fromEnum a
w)


unescapeText :: Text -> Maybe ByteString
unescapeText :: Text -> Maybe ByteString
unescapeText = ByteString -> Text -> Maybe ByteString
go ByteString
forall a. Monoid a => a
mempty
 where
 go :: ByteString -> Text -> Maybe ByteString
go ByteString
bs Text
t =
   case Text -> Maybe (Char, Text)
Text.uncons Text
t of
     Maybe (Char, Text)
Nothing -> ByteString -> Maybe ByteString
forall a. a -> Maybe a
Just ByteString
bs
     Just (Char
c, Text
t')
       | Bool -> Bool
not (Char -> Bool
isAscii Char
c) -> Maybe ByteString
forall a. Maybe a
Nothing
       | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\\'       -> ByteString -> Text -> Maybe ByteString
readEscape ByteString
bs Text
t'
       | Bool
otherwise       -> ByteString -> Char -> Text -> Maybe ByteString
continue ByteString
bs Char
c Text
t'

 continue :: ByteString -> Char -> Text -> Maybe ByteString
continue ByteString
bs Char
c Text
t = ByteString -> Text -> Maybe ByteString
go (ByteString -> Word8 -> ByteString
BS.snoc ByteString
bs (Int -> Word8
forall a. Enum a => Int -> a
toEnum (Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c))) Text
t

 readEscape :: ByteString -> Text -> Maybe ByteString
readEscape ByteString
bs Text
t =
   case Text -> Maybe (Char, Text)
Text.uncons Text
t of
     Maybe (Char, Text)
Nothing -> Maybe ByteString
forall a. Maybe a
Nothing
     Just (Char
c, Text
t')
       | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'a'  -> ByteString -> Char -> Text -> Maybe ByteString
continue ByteString
bs Char
'\a' Text
t'
       | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'b'  -> ByteString -> Char -> Text -> Maybe ByteString
continue ByteString
bs Char
'\b' Text
t'
       | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'e'  -> ByteString -> Char -> Text -> Maybe ByteString
continue ByteString
bs Char
'\x1B' Text
t'
       | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'f'  -> ByteString -> Char -> Text -> Maybe ByteString
continue ByteString
bs Char
'\f' Text
t'
       | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'n'  -> ByteString -> Char -> Text -> Maybe ByteString
continue ByteString
bs Char
'\n' Text
t'
       | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'r'  -> ByteString -> Char -> Text -> Maybe ByteString
continue ByteString
bs Char
'\r' Text
t'
       | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
't'  -> ByteString -> Char -> Text -> Maybe ByteString
continue ByteString
bs Char
'\t' Text
t'
       | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'v'  -> ByteString -> Char -> Text -> Maybe ByteString
continue ByteString
bs Char
'\v' Text
t'
       | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'x'  -> ByteString -> Text -> Maybe ByteString
readHexEscape ByteString
bs Text
t'
       | Bool
otherwise -> ByteString -> Char -> Text -> Maybe ByteString
continue ByteString
bs Char
c Text
t'

 readHexEscape :: ByteString -> Text -> Maybe ByteString
readHexEscape ByteString
bs Text
t =
   case ReadS Int
forall a. (Eq a, Num a) => ReadS a
readHex (Text -> String
Text.unpack (Int -> Text -> Text
Text.take Int
2 Text
t)) of
     (Int
n, []):[(Int, String)]
_ | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
256 -> ByteString -> Text -> Maybe ByteString
go (ByteString -> Word8 -> ByteString
BS.snoc ByteString
bs (Int -> Word8
forall a. Enum a => Int -> a
toEnum Int
n)) (Int -> Text -> Text
Text.drop Int
2 Text
t)
     [(Int, String)]
_ -> Maybe ByteString
forall a. Maybe a
Nothing

-- | This class exists so that solvers supporting the SMTLib2 format can support
--   features that go slightly beyond the standard.
--
-- In particular, there is no standardized syntax for constant arrays (arrays
-- which map every index to the same value).  Solvers that support the theory of
-- arrays and have custom syntax for constant arrays should implement
-- `smtlib2arrayConstant`.  In addition, solvers may override the default
-- representation of complex numbers if necessary.  The default is to represent
-- complex numbers as "(Array Bool Real)" and to build instances by updating a
-- constant array.
class Show a => SMTLib2Tweaks a where
  smtlib2tweaks :: a

  smtlib2exitCommand :: Maybe SMT2.Command
  smtlib2exitCommand = Command -> Maybe Command
forall a. a -> Maybe a
Just Command
SMT2.exit

  -- | Return a representation of the type associated with a (multi-dimensional) symbolic
  -- array.
  --
  -- By default, we encode symbolic arrays using a nested representation.  If the solver,
  -- supports tuples/structs it may wish to change this.
  smtlib2arrayType :: [SMT2.Sort] -> SMT2.Sort -> SMT2.Sort
  smtlib2arrayType [Sort]
l Sort
r = (Sort -> Sort -> Sort) -> Sort -> [Sort] -> Sort
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Sort
i Sort
v -> Sort -> Sort -> Sort
SMT2.arraySort Sort
i Sort
v) Sort
r [Sort]
l

  smtlib2arrayConstant :: Maybe ([SMT2.Sort] -> SMT2.Sort -> Term -> Term)
  smtlib2arrayConstant = Maybe ([Sort] -> Sort -> Term -> Term)
forall a. Maybe a
Nothing

  smtlib2arraySelect :: Term -> [Term] -> Term
  smtlib2arraySelect Term
a [] = Term
a
  smtlib2arraySelect Term
a (Term
h:[Term]
l) = Term -> [Term] -> Term
forall a. SMTLib2Tweaks a => Term -> [Term] -> Term
smtlib2arraySelect @a (Term -> Term -> Term
What4.Protocol.SMTLib2.arraySelect Term
a Term
h) [Term]
l

  smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term
  smtlib2arrayUpdate Term
a [Term]
i Term
v =
    case [Term]
i of
      [] -> String -> Term
forall a. HasCallStack => String -> a
error String
"arrayUpdate given empty list"
      Term
i1:[Term]
ir -> Term -> (Term, [Term]) -> Term -> Term
nestedArrayUpdate Term
a (Term
i1, [Term]
ir) Term
v

  smtlib2StringSort :: SMT2.Sort
  smtlib2StringSort = Builder -> Sort
SMT2.Sort Builder
"String"

  smtlib2StringTerm :: ByteString -> Term
  smtlib2StringTerm = ByteString -> Term
byteStringTerm

  smtlib2StringLength :: Term -> Term
  smtlib2StringLength = Builder -> Term -> Term
SMT2.un_app Builder
"str.len"

  smtlib2StringAppend :: [Term] -> Term
  smtlib2StringAppend = Builder -> [Term] -> Term
SMT2.term_app Builder
"str.++"

  smtlib2StringContains :: Term -> Term -> Term
  smtlib2StringContains = Builder -> Term -> Term -> Term
SMT2.bin_app Builder
"str.contains"

  smtlib2StringIndexOf :: Term -> Term -> Term -> Term
  smtlib2StringIndexOf Term
s Term
t Term
i = Builder -> [Term] -> Term
SMT2.term_app Builder
"str.indexof" [Item [Term]
Term
s,Item [Term]
Term
t,Item [Term]
Term
i]

  smtlib2StringIsPrefixOf :: Term -> Term -> Term
  smtlib2StringIsPrefixOf = Builder -> Term -> Term -> Term
SMT2.bin_app Builder
"str.prefixof"

  smtlib2StringIsSuffixOf :: Term -> Term -> Term
  smtlib2StringIsSuffixOf = Builder -> Term -> Term -> Term
SMT2.bin_app Builder
"str.suffixof"

  smtlib2StringSubstring :: Term -> Term -> Term -> Term
  smtlib2StringSubstring Term
x Term
off Term
len = Builder -> [Term] -> Term
SMT2.term_app Builder
"str.substr" [Item [Term]
Term
x,Item [Term]
Term
off,Item [Term]
Term
len]

  -- | The sort of structs with the given field types.
  --
  -- By default, this uses SMTLIB2 datatypes and are not primitive to the language.
  smtlib2StructSort :: [SMT2.Sort] -> SMT2.Sort
  smtlib2StructSort [] = Builder -> Sort
SMT2.Sort Builder
"Struct0"
  smtlib2StructSort [Sort]
flds = Builder -> Sort
SMT2.Sort (Builder -> Sort) -> Builder -> Sort
forall a b. (a -> b) -> a -> b
$ Builder
"(Struct" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
forall a. Integral a => a -> Builder
Builder.decimal Int
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (Sort -> Builder) -> [Sort] -> Builder
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Sort -> Builder
f [Sort]
flds Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
       where f :: SMT2.Sort -> Builder
             f :: Sort -> Builder
f (SMT2.Sort Builder
s) = Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
s
             n :: Int
n = [Sort] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Sort]
flds

  -- | Construct a struct value from the given field values
  smtlib2StructCtor :: [Term] -> Term
  smtlib2StructCtor [Term]
args = Builder -> [Term] -> Term
term_app Builder
nm [Term]
args
    where nm :: Builder
nm = Builder
"mk-struct" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
forall a. Integral a => a -> Builder
Builder.decimal ([Term] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Term]
args)

  -- | Construct a struct field projection term
  smtlib2StructProj ::
    Int {- ^ number of fields in the struct -} ->
    Int {- ^ 0-based index of the struct field -} ->
    Term {- ^ struct term to project from -} ->
    Term
  smtlib2StructProj Int
n Int
i Term
a = Builder -> [Term] -> Term
term_app Builder
nm [Item [Term]
Term
a]
    where nm :: Builder
nm = Builder
"struct" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
forall a. Integral a => a -> Builder
Builder.decimal Int
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"-proj" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
forall a. Integral a => a -> Builder
Builder.decimal Int
i

  -- By default, this uses the SMTLib 2.6 standard version of the declare-datatype command.
  smtlib2declareStructCmd :: Int -> Maybe SMT2.Command
  smtlib2declareStructCmd Int
0 = Command -> Maybe Command
forall a. a -> Maybe a
Just (Command -> Maybe Command) -> Command -> Maybe Command
forall a b. (a -> b) -> a -> b
$
    Builder -> Command
SMT2.Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-datatype" [ String -> Builder
forall a. IsString a => String -> a
fromString String
"Struct0", [Builder] -> Builder
builder_list [ [Builder] -> Builder
builder_list [Item [Builder]
"mk-struct0"]]]
  smtlib2declareStructCmd Int
n = Command -> Maybe Command
forall a. a -> Maybe a
Just (Command -> Maybe Command) -> Command -> Maybe Command
forall a b. (a -> b) -> a -> b
$
    let n_str :: Builder
n_str = String -> Builder
forall a. IsString a => String -> a
fromString (Int -> String
forall a. Show a => a -> String
show Int
n)
        tp :: Builder
tp = Builder
"Struct" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
n_str
        cnstr :: Builder
cnstr = Builder
"mk-struct" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
n_str
        idxes :: [Builder]
idxes = (Int -> Builder) -> [Int] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Builder
forall a. IsString a => String -> a
fromString (String -> Builder) -> (Int -> String) -> Int -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) [Item [Int]
0 .. Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
        tp_names :: [Builder]
tp_names = [ Builder
"T" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
i_str
                   | Builder
i_str <- [Builder]
idxes
                   ]
        flds :: [Builder]
flds = [ Builder -> [Builder] -> Builder
app (Builder
"struct" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
n_str Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"-proj" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
i_str) [ Builder
"T" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
i_str ]
               | Builder
i_str <- [Builder]
idxes
               ]
     in Builder -> Command
SMT2.Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-datatype" [ Item [Builder]
Builder
tp, Builder -> [Builder] -> Builder
app Builder
"par" [ [Builder] -> Builder
builder_list [Builder]
tp_names, [Builder] -> Builder
builder_list [Builder -> [Builder] -> Builder
app Builder
cnstr [Builder]
flds]]]



asSMT2Type :: forall a tp . SMTLib2Tweaks a => TypeMap tp -> SMT2.Sort
asSMT2Type :: TypeMap tp -> Sort
asSMT2Type TypeMap tp
BoolTypeMap    = Sort
SMT2.boolSort
asSMT2Type TypeMap tp
IntegerTypeMap = Sort
SMT2.intSort
asSMT2Type TypeMap tp
RealTypeMap    = Sort
SMT2.realSort
asSMT2Type (BVTypeMap NatRepr w
w)  = Natural -> Sort
SMT2.bvSort (NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w)
asSMT2Type (FloatTypeMap FloatPrecisionRepr fpp
fpp) = Builder -> Sort
SMT2.Sort (Builder -> Sort) -> Builder -> Sort
forall a b. (a -> b) -> a -> b
$ Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"FloatingPoint" (FloatPrecisionRepr fpp -> SMTFloatPrecision
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)
asSMT2Type TypeMap tp
Char8TypeMap = SMTLib2Tweaks a => Sort
forall a. SMTLib2Tweaks a => Sort
smtlib2StringSort @a
asSMT2Type TypeMap tp
ComplexToStructTypeMap =
  [Sort] -> Sort
forall a. SMTLib2Tweaks a => [Sort] -> Sort
smtlib2StructSort @a [ Item [Sort]
Sort
SMT2.realSort, Item [Sort]
Sort
SMT2.realSort ]
asSMT2Type TypeMap tp
ComplexToArrayTypeMap =
  [Sort] -> Sort -> Sort
forall a. SMTLib2Tweaks a => [Sort] -> Sort -> Sort
smtlib2arrayType @a [Item [Sort]
Sort
SMT2.boolSort] Sort
SMT2.realSort
asSMT2Type (PrimArrayTypeMap Assignment TypeMap (idxl ::> idx)
i TypeMap tp
r) =
  [Sort] -> Sort -> Sort
forall a. SMTLib2Tweaks a => [Sort] -> Sort -> Sort
smtlib2arrayType @a ((forall (x :: BaseType). TypeMap x -> Sort)
-> Assignment TypeMap (idxl ::> idx) -> [Sort]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC (forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
forall (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a) Assignment TypeMap (idxl ::> idx)
i) (TypeMap tp -> Sort
forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap tp
r)
asSMT2Type (FnArrayTypeMap Assignment TypeMap (idxl ::> idx)
_ TypeMap tp
_) =
  String -> Sort
forall a. HasCallStack => String -> a
error String
"SMTLIB backend does not support function types as first class."
asSMT2Type (StructTypeMap Assignment TypeMap idx
f) =
  [Sort] -> Sort
forall a. SMTLib2Tweaks a => [Sort] -> Sort
smtlib2StructSort @a ((forall (x :: BaseType). TypeMap x -> Sort)
-> Assignment TypeMap idx -> [Sort]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC (forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
forall (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a) Assignment TypeMap idx
f)

-- Default instance.
instance SMTLib2Tweaks () where
  smtlib2tweaks :: ()
smtlib2tweaks = ()

------------------------------------------------------------------------
readBin :: Num a => ReadS a
readBin :: ReadS a
readBin = a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
readInt a
2 (Char -> String -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` (String
"01" :: String)) Char -> Int
digitToInt

------------------------------------------------------------------------
-- Type

mkRoundingOp :: Builder -> RoundingMode -> Builder
mkRoundingOp :: Builder -> RoundingMode -> Builder
mkRoundingOp Builder
op RoundingMode
r = Builder
op Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. IsString a => String -> a
fromString (RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
r)

------------------------------------------------------------------------
-- Writer

newtype Writer a = Writer { Writer a -> IORef (Set Int)
declaredTuples :: IORef (Set Int) }

type instance SMTWriter.Term (Writer a) = Term

instance Num Term where
  Term
x + :: Term -> Term -> Term
+ Term
y = [Term] -> Term
SMT2.add [Item [Term]
Term
x, Item [Term]
Term
y]
  Term
x - :: Term -> Term -> Term
- Term
y = Term -> [Term] -> Term
SMT2.sub Term
x [Item [Term]
Term
y]
  Term
x * :: Term -> Term -> Term
* Term
y = [Term] -> Term
SMT2.mul [Item [Term]
Term
x, Item [Term]
Term
y]
  negate :: Term -> Term
negate Term
x = Term -> Term
SMT2.negate Term
x
  abs :: Term -> Term
abs Term
x    = Term -> Term -> Term -> Term
SMT2.ite ([Term] -> Term
SMT2.ge [Item [Term]
Term
x, Integer -> Term
SMT2.numeral Integer
0]) Term
x (Term -> Term
SMT2.negate Term
x)
  signum :: Term -> Term
signum Term
x =
    Term -> Term -> Term -> Term
SMT2.ite ([Term] -> Term
SMT2.ge [Item [Term]
Term
x, Integer -> Term
SMT2.numeral Integer
0])
             (Term -> Term -> Term -> Term
SMT2.ite ([Term] -> Term
SMT2.eq [Item [Term]
Term
x, Integer -> Term
SMT2.numeral Integer
0]) (Integer -> Term
SMT2.numeral Integer
0) (Integer -> Term
SMT2.numeral Integer
1))
             (Term -> Term
SMT2.negate (Integer -> Term
SMT2.numeral Integer
1))
  fromInteger :: Integer -> Term
fromInteger = Integer -> Term
SMT2.numeral

varBinding :: forall a . SMTLib2Tweaks a => (Text, Some TypeMap) -> (Text, SMT2.Sort)
varBinding :: (Text, Some TypeMap) -> (Text, Sort)
varBinding (Text
nm, Some TypeMap x
tp) = (Text
nm, TypeMap x -> Sort
forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap x
tp)

-- The SMTLIB2 exporter uses the datatypes theory for representing structures.
--
-- Note about structs:
--
-- For each length XX associated to some structure with that length in the
-- formula, the SMTLIB2 backend defines a datatype "StructXX" with the
-- constructor "mk-structXX", and projection operations "structXX-projII"
-- for II an natural number less than XX.
instance SupportTermOps Term where
  boolExpr :: Bool -> Term
boolExpr Bool
b = if Bool
b then Term
SMT2.true else Term
SMT2.false
  notExpr :: Term -> Term
notExpr = Term -> Term
SMT2.not

  andAll :: [Term] -> Term
andAll = [Term] -> Term
SMT2.and
  orAll :: [Term] -> Term
orAll  = [Term] -> Term
SMT2.or

  Term
x .== :: Term -> Term -> Term
.== Term
y = [Term] -> Term
SMT2.eq [Item [Term]
Term
x,Item [Term]
Term
y]
  Term
x ./= :: Term -> Term -> Term
./= Term
y = [Term] -> Term
SMT2.distinct [Item [Term]
Term
x,Item [Term]
Term
y]

  -- NB: SMT2.letBinder defines a "parallel" let, and
  -- we want the semantics of a "sequential" let, so expand
  -- to a series of nested lets.
  letExpr :: [(Text, Term)] -> Term -> Term
letExpr [(Text, Term)]
vs Term
t = ((Text, Term) -> Term -> Term) -> Term -> [(Text, Term)] -> Term
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Text, Term)
v -> [(Text, Term)] -> Term -> Term
SMT2.letBinder [(Text, Term)
Item [(Text, Term)]
v]) Term
t [(Text, Term)]
vs

  ite :: Term -> Term -> Term -> Term
ite = Term -> Term -> Term -> Term
SMT2.ite

  sumExpr :: [Term] -> Term
sumExpr = [Term] -> Term
SMT2.add

  termIntegerToReal :: Term -> Term
termIntegerToReal = Term -> Term
SMT2.toReal
  termRealToInteger :: Term -> Term
termRealToInteger = Term -> Term
SMT2.toInt

  integerTerm :: Integer -> Term
integerTerm = Integer -> Term
SMT2.numeral
  intDiv :: Term -> Term -> Term
intDiv Term
x Term
y = Term -> [Term] -> Term
SMT2.div Term
x [Item [Term]
Term
y]
  intMod :: Term -> Term -> Term
intMod = Term -> Term -> Term
SMT2.mod
  intAbs :: Term -> Term
intAbs     = Term -> Term
SMT2.abs

  intDivisible :: Term -> Natural -> Term
intDivisible Term
x Natural
0 = Term
x Term -> Term -> Term
forall v. SupportTermOps v => v -> v -> v
.== Integer -> Term
forall v. SupportTermOps v => Integer -> v
integerTerm Integer
0
  intDivisible Term
x Natural
k = Term -> Term -> Term
forall v. SupportTermOps v => v -> v -> v
intMod Term
x (Integer -> Term
forall v. SupportTermOps v => Integer -> v
integerTerm (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
k)) Term -> Term -> Term
forall v. SupportTermOps v => v -> v -> v
.== Term
0

  rationalTerm :: Rational -> Term
rationalTerm Rational
r | Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1    = Integer -> Term
SMT2.decimal Integer
n
                 | Bool
otherwise = (Integer -> Term
SMT2.decimal Integer
n) Term -> [Term] -> Term
SMT2../ [Integer -> Term
SMT2.decimal Integer
d]
    where n :: Integer
n = Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r
          d :: Integer
d = Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r

  Term
x .< :: Term -> Term -> Term
.<  Term
y = [Term] -> Term
SMT2.lt [Item [Term]
Term
x,Item [Term]
Term
y]
  Term
x .<= :: Term -> Term -> Term
.<= Term
y = [Term] -> Term
SMT2.le [Item [Term]
Term
x,Item [Term]
Term
y]
  Term
x .> :: Term -> Term -> Term
.>  Term
y = [Term] -> Term
SMT2.gt [Item [Term]
Term
x,Item [Term]
Term
y]
  Term
x .>= :: Term -> Term -> Term
.>= Term
y = [Term] -> Term
SMT2.ge [Item [Term]
Term
x,Item [Term]
Term
y]

  bvTerm :: NatRepr w -> BV w -> Term
bvTerm NatRepr w
w BV w
u = case NatRepr w -> Either (w :~: 0) (LeqProof 1 w)
forall (n :: Nat). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr w
w of
    Left w :~: 0
Refl -> String -> Term
forall a. HasCallStack => String -> a
error String
"Cannot construct BV term with 0 width"
    Right LeqProof 1 w
LeqProof -> NatRepr w -> BV w -> Term
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Term
SMT2.bvdecimal NatRepr w
w BV w
u

  bvNeg :: Term -> Term
bvNeg = Term -> Term
SMT2.bvneg
  bvAdd :: Term -> Term -> Term
bvAdd Term
x Term
y = Term -> [Term] -> Term
SMT2.bvadd Term
x [Item [Term]
Term
y]
  bvSub :: Term -> Term -> Term
bvSub = Term -> Term -> Term
SMT2.bvsub
  bvMul :: Term -> Term -> Term
bvMul Term
x Term
y = Term -> [Term] -> Term
SMT2.bvmul Term
x [Item [Term]
Term
y]

  bvSLe :: Term -> Term -> Term
bvSLe = Term -> Term -> Term
SMT2.bvsle
  bvULe :: Term -> Term -> Term
bvULe = Term -> Term -> Term
SMT2.bvule

  bvSLt :: Term -> Term -> Term
bvSLt = Term -> Term -> Term
SMT2.bvslt
  bvULt :: Term -> Term -> Term
bvULt = Term -> Term -> Term
SMT2.bvult

  bvUDiv :: Term -> Term -> Term
bvUDiv = Term -> Term -> Term
SMT2.bvudiv
  bvURem :: Term -> Term -> Term
bvURem = Term -> Term -> Term
SMT2.bvurem
  bvSDiv :: Term -> Term -> Term
bvSDiv = Term -> Term -> Term
SMT2.bvsdiv
  bvSRem :: Term -> Term -> Term
bvSRem = Term -> Term -> Term
SMT2.bvsrem

  bvNot :: Term -> Term
bvNot = Term -> Term
SMT2.bvnot
  bvAnd :: Term -> Term -> Term
bvAnd Term
x Term
y = Term -> [Term] -> Term
SMT2.bvand Term
x [Item [Term]
Term
y]
  bvOr :: Term -> Term -> Term
bvOr  Term
x Term
y = Term -> [Term] -> Term
SMT2.bvor  Term
x [Item [Term]
Term
y]
  bvXor :: Term -> Term -> Term
bvXor Term
x Term
y = Term -> [Term] -> Term
SMT2.bvxor Term
x [Item [Term]
Term
y]

  bvShl :: Term -> Term -> Term
bvShl  = Term -> Term -> Term
SMT2.bvshl
  bvLshr :: Term -> Term -> Term
bvLshr = Term -> Term -> Term
SMT2.bvlshr
  bvAshr :: Term -> Term -> Term
bvAshr = Term -> Term -> Term
SMT2.bvashr

  bvConcat :: Term -> Term -> Term
bvConcat = Term -> Term -> Term
SMT2.concat

  bvExtract :: NatRepr w -> Natural -> Natural -> Term -> Term
bvExtract NatRepr w
_ Natural
b Natural
n Term
x | Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
0 = Natural -> Natural -> Term -> Term
SMT2.extract (Natural
bNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
+Natural
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
-Natural
1) Natural
b Term
x
                    | Bool
otherwise = String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ String
"bvExtract given non-positive width " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
n

  floatNeg :: Term -> Term
floatNeg  = Builder -> Term -> Term
un_app Builder
"fp.neg"
  floatAbs :: Term -> Term
floatAbs  = Builder -> Term -> Term
un_app Builder
"fp.abs"
  floatSqrt :: RoundingMode -> Term -> Term
floatSqrt RoundingMode
r = Builder -> Term -> Term
un_app (Builder -> Term -> Term) -> Builder -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp Builder
"fp.sqrt " RoundingMode
r

  floatAdd :: RoundingMode -> Term -> Term -> Term
floatAdd RoundingMode
r = Builder -> Term -> Term -> Term
bin_app (Builder -> Term -> Term -> Term)
-> Builder -> Term -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp Builder
"fp.add" RoundingMode
r
  floatSub :: RoundingMode -> Term -> Term -> Term
floatSub RoundingMode
r = Builder -> Term -> Term -> Term
bin_app (Builder -> Term -> Term -> Term)
-> Builder -> Term -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp Builder
"fp.sub" RoundingMode
r
  floatMul :: RoundingMode -> Term -> Term -> Term
floatMul RoundingMode
r = Builder -> Term -> Term -> Term
bin_app (Builder -> Term -> Term -> Term)
-> Builder -> Term -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp Builder
"fp.mul" RoundingMode
r
  floatDiv :: RoundingMode -> Term -> Term -> Term
floatDiv RoundingMode
r = Builder -> Term -> Term -> Term
bin_app (Builder -> Term -> Term -> Term)
-> Builder -> Term -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp Builder
"fp.div" RoundingMode
r
  floatRem :: Term -> Term -> Term
floatRem = Builder -> Term -> Term -> Term
bin_app Builder
"fp.rem"

  floatFMA :: RoundingMode -> Term -> Term -> Term -> Term
floatFMA RoundingMode
r Term
x Term
y Term
z = Builder -> [Term] -> Term
term_app (Builder -> RoundingMode -> Builder
mkRoundingOp Builder
"fp.fma" RoundingMode
r) [Item [Term]
Term
x, Item [Term]
Term
y, Item [Term]
Term
z]

  floatEq :: Term -> Term -> Term
floatEq Term
x Term
y  = [Term] -> Term
SMT2.eq [Item [Term]
Term
x,Item [Term]
Term
y]
  floatFpEq :: Term -> Term -> Term
floatFpEq = Builder -> Term -> Term -> Term
bin_app Builder
"fp.eq"
  floatLe :: Term -> Term -> Term
floatLe   = Builder -> Term -> Term -> Term
bin_app Builder
"fp.leq"
  floatLt :: Term -> Term -> Term
floatLt   = Builder -> Term -> Term -> Term
bin_app Builder
"fp.lt"

  floatIsNaN :: Term -> Term
floatIsNaN      = Builder -> Term -> Term
un_app Builder
"fp.isNaN"
  floatIsInf :: Term -> Term
floatIsInf      = Builder -> Term -> Term
un_app Builder
"fp.isInfinite"
  floatIsZero :: Term -> Term
floatIsZero     = Builder -> Term -> Term
un_app Builder
"fp.isZero"
  floatIsPos :: Term -> Term
floatIsPos      = Builder -> Term -> Term
un_app Builder
"fp.isPositive"
  floatIsNeg :: Term -> Term
floatIsNeg      = Builder -> Term -> Term
un_app Builder
"fp.isNegative"
  floatIsSubnorm :: Term -> Term
floatIsSubnorm  = Builder -> Term -> Term
un_app Builder
"fp.isSubnormal"
  floatIsNorm :: Term -> Term
floatIsNorm     = Builder -> Term -> Term
un_app Builder
"fp.isNormal"

  floatTerm :: FloatPrecisionRepr fpp -> BigFloat -> Term
floatTerm fpp :: FloatPrecisionRepr fpp
fpp@(FloatingPointPrecisionRepr NatRepr eb
eb NatRepr sb
sb) BigFloat
bf =
      Builder -> Term -> Term
un_app (Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"to_fp" (FloatPrecisionRepr fpp -> SMTFloatPrecision
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)) (NatRepr (eb + sb) -> BV (eb + sb) -> Term
forall v (w :: Nat). SupportTermOps v => NatRepr w -> BV w -> v
bvTerm NatRepr (eb + sb)
w BV (eb + sb)
bv)
    where
      w :: NatRepr (eb + sb)
w = NatRepr eb -> NatRepr sb -> NatRepr (eb + sb)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr eb
eb NatRepr sb
sb
      bv :: BV (eb + sb)
bv = NatRepr (eb + sb) -> Integer -> BV (eb + sb)
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr (eb + sb)
w (BFOpts -> BigFloat -> Integer
bfToBits (FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
RNE) BigFloat
bf)

  floatCast :: FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term
floatCast FloatPrecisionRepr fpp
fpp RoundingMode
r = Builder -> Term -> Term
un_app (Builder -> Term -> Term) -> Builder -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp (Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"to_fp" (FloatPrecisionRepr fpp -> SMTFloatPrecision
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)) RoundingMode
r
  floatRound :: RoundingMode -> Term -> Term
floatRound RoundingMode
r = Builder -> Term -> Term
un_app (Builder -> Term -> Term) -> Builder -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp Builder
"fp.roundToIntegral" RoundingMode
r
  floatFromBinary :: FloatPrecisionRepr fpp -> Term -> Term
floatFromBinary FloatPrecisionRepr fpp
fpp = Builder -> Term -> Term
un_app (Builder -> Term -> Term) -> Builder -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"to_fp" (FloatPrecisionRepr fpp -> SMTFloatPrecision
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)
  bvToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term
bvToFloat FloatPrecisionRepr fpp
fpp RoundingMode
r =
    Builder -> Term -> Term
un_app (Builder -> Term -> Term) -> Builder -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp (Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"to_fp_unsigned" (FloatPrecisionRepr fpp -> SMTFloatPrecision
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)) RoundingMode
r
  sbvToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term
sbvToFloat FloatPrecisionRepr fpp
fpp RoundingMode
r = Builder -> Term -> Term
un_app (Builder -> Term -> Term) -> Builder -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp (Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"to_fp" (FloatPrecisionRepr fpp -> SMTFloatPrecision
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)) RoundingMode
r
  realToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term
realToFloat FloatPrecisionRepr fpp
fpp RoundingMode
r = Builder -> Term -> Term
un_app (Builder -> Term -> Term) -> Builder -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp (Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"to_fp" (FloatPrecisionRepr fpp -> SMTFloatPrecision
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)) RoundingMode
r

  floatToBV :: Natural -> RoundingMode -> Term -> Term
floatToBV Natural
w RoundingMode
r =
    Builder -> Term -> Term
un_app (Builder -> Term -> Term) -> Builder -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp (Builder
"(_ fp.to_ubv " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. IsString a => String -> a
fromString (Natural -> String
forall a. Show a => a -> String
show Natural
w) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")") RoundingMode
r
  floatToSBV :: Natural -> RoundingMode -> Term -> Term
floatToSBV Natural
w RoundingMode
r =
    Builder -> Term -> Term
un_app (Builder -> Term -> Term) -> Builder -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp (Builder
"(_ fp.to_sbv " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. IsString a => String -> a
fromString (Natural -> String
forall a. Show a => a -> String
show Natural
w) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")") RoundingMode
r

  floatToReal :: Term -> Term
floatToReal = Builder -> Term -> Term
un_app Builder
"fp.to_real"

  realIsInteger :: Term -> Term
realIsInteger = Term -> Term
SMT2.isInt

  realDiv :: Term -> Term -> Term
realDiv Term
x Term
y = Term
x Term -> [Term] -> Term
SMT2../ [Item [Term]
Term
y]
  realSin :: Term -> Term
realSin = Builder -> Term -> Term
un_app Builder
"sin"
  realCos :: Term -> Term
realCos = Builder -> Term -> Term
un_app Builder
"cos"
  realATan2 :: Term -> Term -> Term
realATan2 = Builder -> Term -> Term -> Term
bin_app Builder
"atan2"
  realSinh :: Term -> Term
realSinh = Builder -> Term -> Term
un_app Builder
"sinh"
  realCosh :: Term -> Term
realCosh = Builder -> Term -> Term
un_app Builder
"cosh"
  realExp :: Term -> Term
realExp = Builder -> Term -> Term
un_app Builder
"exp"
  realLog :: Term -> Term
realLog = Builder -> Term -> Term
un_app Builder
"log"

  smtFnApp :: Term -> [Term] -> Term
smtFnApp Term
nm [Term]
args = Builder -> [Term] -> Term
term_app (Term -> Builder
SMT2.renderTerm Term
nm) [Term]
args

  fromText :: Text -> Term
fromText Text
t = Builder -> Term
SMT2.T (Text -> Builder
Builder.fromText Text
t)

------------------------------------------------------------------------
-- Writer

newWriter :: a
          -> Streams.OutputStream Text
             -- ^ Stream to write queries onto
          -> Streams.InputStream Text
              -- ^ Input stream to read responses from
              --   (may be the @nullInput@ stream if no responses are expected)
          -> AcknowledgementAction t (Writer a)
             -- ^ Action to run for consuming acknowledgement messages
          -> String
             -- ^ Name of solver for reporting purposes.
          -> Bool
             -- ^ Flag indicating if it is permitted to use
             -- "define-fun" when generating SMTLIB
          -> ProblemFeatures
             -- ^ Indicates what features are supported by the solver
          -> Bool
             -- ^ Indicates if quantifiers are supported.
          -> B.SymbolVarBimap t
             -- ^ Variable bindings for names.
          -> IO (WriterConn t (Writer a))
newWriter :: a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
newWriter a
_ OutputStream Text
h InputStream Text
in_h AcknowledgementAction t (Writer a)
ack String
solver_name Bool
permitDefineFun ProblemFeatures
arithOption Bool
quantSupport SymbolVarBimap t
bindings = do
  IORef (Set Int)
r <- Set Int -> IO (IORef (Set Int))
forall a. a -> IO (IORef a)
newIORef Set Int
forall a. Set a
Set.empty
  let initWriter :: Writer a
initWriter =
        Writer :: forall a. IORef (Set Int) -> Writer a
Writer
        { declaredTuples :: IORef (Set Int)
declaredTuples = IORef (Set Int)
r
        }
  WriterConn t (Writer a)
conn <- OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> String
-> ProblemFeatures
-> SymbolVarBimap t
-> Writer a
-> IO (WriterConn t (Writer a))
forall t cs.
OutputStream Text
-> InputStream Text
-> AcknowledgementAction t cs
-> String
-> ProblemFeatures
-> SymbolVarBimap t
-> cs
-> IO (WriterConn t cs)
newWriterConn OutputStream Text
h InputStream Text
in_h AcknowledgementAction t (Writer a)
ack String
solver_name ProblemFeatures
arithOption SymbolVarBimap t
bindings Writer a
initWriter
  WriterConn t (Writer a) -> IO (WriterConn t (Writer a))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (WriterConn t (Writer a) -> IO (WriterConn t (Writer a)))
-> WriterConn t (Writer a) -> IO (WriterConn t (Writer a))
forall a b. (a -> b) -> a -> b
$! WriterConn t (Writer a)
conn { supportFunctionDefs :: Bool
supportFunctionDefs = Bool
permitDefineFun
                 , supportQuantifiers :: Bool
supportQuantifiers = Bool
quantSupport
                 }

type instance Command (Writer a) = SMT2.Command

instance SMTLib2Tweaks a => SMTWriter (Writer a) where
  forallExpr :: [(Text, Some TypeMap)] -> Term (Writer a) -> Term (Writer a)
forallExpr [(Text, Some TypeMap)]
vars Term (Writer a)
t = [(Text, Sort)] -> Term -> Term
SMT2.forall (SMTLib2Tweaks a => (Text, Some TypeMap) -> (Text, Sort)
forall a. SMTLib2Tweaks a => (Text, Some TypeMap) -> (Text, Sort)
varBinding @a ((Text, Some TypeMap) -> (Text, Sort))
-> [(Text, Some TypeMap)] -> [(Text, Sort)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
vars) Term
Term (Writer a)
t
  existsExpr :: [(Text, Some TypeMap)] -> Term (Writer a) -> Term (Writer a)
existsExpr [(Text, Some TypeMap)]
vars Term (Writer a)
t = [(Text, Sort)] -> Term -> Term
SMT2.exists (SMTLib2Tweaks a => (Text, Some TypeMap) -> (Text, Sort)
forall a. SMTLib2Tweaks a => (Text, Some TypeMap) -> (Text, Sort)
varBinding @a ((Text, Some TypeMap) -> (Text, Sort))
-> [(Text, Some TypeMap)] -> [(Text, Sort)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
vars) Term
Term (Writer a)
t

  arrayConstant :: Maybe (ArrayConstantFn (Term (Writer a)))
arrayConstant =
    case SMTLib2Tweaks a => Maybe ([Sort] -> Sort -> Term -> Term)
forall a. SMTLib2Tweaks a => Maybe ([Sort] -> Sort -> Term -> Term)
smtlib2arrayConstant @a of
      Just [Sort] -> Sort -> Term -> Term
f -> ([Some TypeMap] -> Some TypeMap -> Term -> Term)
-> Maybe ([Some TypeMap] -> Some TypeMap -> Term -> Term)
forall a. a -> Maybe a
Just (([Some TypeMap] -> Some TypeMap -> Term -> Term)
 -> Maybe ([Some TypeMap] -> Some TypeMap -> Term -> Term))
-> ([Some TypeMap] -> Some TypeMap -> Term -> Term)
-> Maybe ([Some TypeMap] -> Some TypeMap -> Term -> Term)
forall a b. (a -> b) -> a -> b
$ \[Some TypeMap]
idxTypes (Some TypeMap x
retType) Term
c ->
        [Sort] -> Sort -> Term -> Term
f ((\(Some TypeMap x
itp) -> TypeMap x -> Sort
forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap x
itp) (Some TypeMap -> Sort) -> [Some TypeMap] -> [Sort]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Some TypeMap]
idxTypes) (TypeMap x -> Sort
forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap x
retType) Term
c
      Maybe ([Sort] -> Sort -> Term -> Term)
Nothing -> Maybe (ArrayConstantFn (Term (Writer a)))
forall a. Maybe a
Nothing
  arraySelect :: Term (Writer a) -> [Term (Writer a)] -> Term (Writer a)
arraySelect = SMTLib2Tweaks a => Term -> [Term] -> Term
forall a. SMTLib2Tweaks a => Term -> [Term] -> Term
smtlib2arraySelect @a
  arrayUpdate :: Term (Writer a)
-> [Term (Writer a)] -> Term (Writer a) -> Term (Writer a)
arrayUpdate = SMTLib2Tweaks a => Term -> [Term] -> Term -> Term
forall a. SMTLib2Tweaks a => Term -> [Term] -> Term -> Term
smtlib2arrayUpdate @a

  commentCommand :: f (Writer a) -> Builder -> Command (Writer a)
commentCommand f (Writer a)
_ Builder
b = Builder -> Command
SMT2.Cmd (Builder
"; " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
b)

  assertCommand :: f (Writer a) -> Term (Writer a) -> Command (Writer a)
assertCommand f (Writer a)
_ Term (Writer a)
e = Term -> Command
SMT2.assert Term
Term (Writer a)
e

  assertNamedCommand :: f (Writer a) -> Term (Writer a) -> Text -> Command (Writer a)
assertNamedCommand f (Writer a)
_ Term (Writer a)
e Text
nm = Term -> Text -> Command
SMT2.assertNamed Term
Term (Writer a)
e Text
nm

  pushCommand :: f (Writer a) -> Command (Writer a)
pushCommand f (Writer a)
_  = Integer -> Command
SMT2.push Integer
1
  popCommand :: f (Writer a) -> Command (Writer a)
popCommand f (Writer a)
_   = Integer -> Command
SMT2.pop Integer
1
  resetCommand :: f (Writer a) -> Command (Writer a)
resetCommand f (Writer a)
_ = Command
Command (Writer a)
SMT2.resetAssertions
  popManyCommands :: f (Writer a) -> Int -> [Command (Writer a)]
popManyCommands f (Writer a)
_ Int
n = [Integer -> Command
SMT2.pop (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)]

  checkCommands :: f (Writer a) -> [Command (Writer a)]
checkCommands f (Writer a)
_ = [Item [Command]
Command
SMT2.checkSat]
  checkWithAssumptionsCommands :: f (Writer a) -> [Text] -> [Command (Writer a)]
checkWithAssumptionsCommands f (Writer a)
_ [Text]
nms = [[Text] -> Command
SMT2.checkSatWithAssumptions [Text]
nms]

  getUnsatAssumptionsCommand :: f (Writer a) -> Command (Writer a)
getUnsatAssumptionsCommand f (Writer a)
_ = Command
Command (Writer a)
SMT2.getUnsatAssumptions
  getUnsatCoreCommand :: f (Writer a) -> Command (Writer a)
getUnsatCoreCommand f (Writer a)
_ = Command
Command (Writer a)
SMT2.getUnsatCore
  setOptCommand :: f (Writer a) -> Text -> Text -> Command (Writer a)
setOptCommand f (Writer a)
_ = Text -> Text -> Command
Text -> Text -> Command (Writer a)
SMT2.setOption

  declareCommand :: f (Writer a)
-> Text
-> Assignment TypeMap args
-> TypeMap rtp
-> Command (Writer a)
declareCommand f (Writer a)
_proxy Text
v Assignment TypeMap args
argTypes TypeMap rtp
retType =
    Text -> [Sort] -> Sort -> Command
SMT2.declareFun Text
v ((forall (x :: BaseType). TypeMap x -> Sort)
-> Assignment TypeMap args -> [Sort]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC (forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
forall (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a) Assignment TypeMap args
argTypes) (TypeMap rtp -> Sort
forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap rtp
retType)

  defineCommand :: f (Writer a)
-> Text
-> [(Text, Some TypeMap)]
-> TypeMap rtp
-> Term (Writer a)
-> Command (Writer a)
defineCommand f (Writer a)
_proxy Text
f [(Text, Some TypeMap)]
args TypeMap rtp
return_type Term (Writer a)
e =
    let resolveArg :: (Text, Some TypeMap) -> (Text, Sort)
resolveArg (Text
var, Some TypeMap x
tp) = (Text
var, TypeMap x -> Sort
forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap x
tp)
     in Text -> [(Text, Sort)] -> Sort -> Term -> Command
SMT2.defineFun Text
f ((Text, Some TypeMap) -> (Text, Sort)
resolveArg ((Text, Some TypeMap) -> (Text, Sort))
-> [(Text, Some TypeMap)] -> [(Text, Sort)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
args) (TypeMap rtp -> Sort
forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap rtp
return_type) Term
Term (Writer a)
e

  stringTerm :: ByteString -> Term (Writer a)
stringTerm ByteString
bs = ByteString -> Term
forall a. SMTLib2Tweaks a => ByteString -> Term
smtlib2StringTerm @a ByteString
bs
  stringLength :: Term (Writer a) -> Term (Writer a)
stringLength Term (Writer a)
x = Term -> Term
forall a. SMTLib2Tweaks a => Term -> Term
smtlib2StringLength @a Term
Term (Writer a)
x
  stringAppend :: [Term (Writer a)] -> Term (Writer a)
stringAppend [Term (Writer a)]
xs = [Term] -> Term
forall a. SMTLib2Tweaks a => [Term] -> Term
smtlib2StringAppend @a [Term]
[Term (Writer a)]
xs
  stringContains :: Term (Writer a) -> Term (Writer a) -> Term (Writer a)
stringContains Term (Writer a)
x Term (Writer a)
y = Term -> Term -> Term
forall a. SMTLib2Tweaks a => Term -> Term -> Term
smtlib2StringContains @a Term
Term (Writer a)
x Term
Term (Writer a)
y
  stringIsPrefixOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a)
stringIsPrefixOf Term (Writer a)
x Term (Writer a)
y = Term -> Term -> Term
forall a. SMTLib2Tweaks a => Term -> Term -> Term
smtlib2StringIsPrefixOf @a Term
Term (Writer a)
x Term
Term (Writer a)
y
  stringIsSuffixOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a)
stringIsSuffixOf Term (Writer a)
x Term (Writer a)
y = Term -> Term -> Term
forall a. SMTLib2Tweaks a => Term -> Term -> Term
smtlib2StringIsSuffixOf @a Term
Term (Writer a)
x Term
Term (Writer a)
y
  stringIndexOf :: Term (Writer a)
-> Term (Writer a) -> Term (Writer a) -> Term (Writer a)
stringIndexOf Term (Writer a)
x Term (Writer a)
y Term (Writer a)
k = Term -> Term -> Term -> Term
forall a. SMTLib2Tweaks a => Term -> Term -> Term -> Term
smtlib2StringIndexOf @a Term
Term (Writer a)
x Term
Term (Writer a)
y Term
Term (Writer a)
k
  stringSubstring :: Term (Writer a)
-> Term (Writer a) -> Term (Writer a) -> Term (Writer a)
stringSubstring Term (Writer a)
x Term (Writer a)
off Term (Writer a)
len = Term -> Term -> Term -> Term
forall a. SMTLib2Tweaks a => Term -> Term -> Term -> Term
smtlib2StringSubstring @a Term
Term (Writer a)
x Term
Term (Writer a)
off Term
Term (Writer a)
len

  structCtor :: Assignment TypeMap args -> [Term (Writer a)] -> Term (Writer a)
structCtor Assignment TypeMap args
_tps [Term (Writer a)]
vals = [Term] -> Term
forall a. SMTLib2Tweaks a => [Term] -> Term
smtlib2StructCtor @a [Term]
[Term (Writer a)]
vals

  structProj :: Assignment TypeMap args
-> Index args tp -> Term (Writer a) -> Term (Writer a)
structProj Assignment TypeMap args
tps Index args tp
idx Term (Writer a)
v =
    let n :: Int
n = Size args -> Int
forall k (ctx :: Ctx k). Size ctx -> Int
Ctx.sizeInt (Assignment TypeMap args -> Size args
forall k (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment TypeMap args
tps)
        i :: Int
i = Index args tp -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal Index args tp
idx
     in Int -> Int -> Term -> Term
forall a. SMTLib2Tweaks a => Int -> Int -> Term -> Term
smtlib2StructProj @a Int
n Int
i Term
Term (Writer a)
v

  resetDeclaredStructs :: WriterConn t (Writer a) -> IO ()
resetDeclaredStructs WriterConn t (Writer a)
conn = do
    let r :: IORef (Set Int)
r = Writer a -> IORef (Set Int)
forall a. Writer a -> IORef (Set Int)
declaredTuples (WriterConn t (Writer a) -> Writer a
forall t h. WriterConn t h -> h
connState WriterConn t (Writer a)
conn)
    IORef (Set Int) -> Set Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Set Int)
r Set Int
forall a. Monoid a => a
mempty

  declareStructDatatype :: WriterConn t (Writer a) -> Assignment TypeMap args -> IO ()
declareStructDatatype WriterConn t (Writer a)
conn Assignment TypeMap args
flds = do
    let n :: Int
n = Size args -> Int
forall k (ctx :: Ctx k). Size ctx -> Int
Ctx.sizeInt (Assignment TypeMap args -> Size args
forall k (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment TypeMap args
flds)
    let r :: IORef (Set Int)
r = Writer a -> IORef (Set Int)
forall a. Writer a -> IORef (Set Int)
declaredTuples (WriterConn t (Writer a) -> Writer a
forall t h. WriterConn t h -> h
connState WriterConn t (Writer a)
conn)
    Set Int
s <- IORef (Set Int) -> IO (Set Int)
forall a. IORef a -> IO a
readIORef IORef (Set Int)
r
    Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Int
n Set Int
s) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      case Int -> Maybe Command
forall a. SMTLib2Tweaks a => Int -> Maybe Command
smtlib2declareStructCmd @a Int
n of
        Maybe Command
Nothing -> () -> IO ()
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
        Just Command
cmd -> WriterConn t (Writer a) -> Command (Writer a) -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t (Writer a)
conn Command
Command (Writer a)
cmd
      IORef (Set Int) -> Set Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Set Int)
r (Set Int -> IO ()) -> Set Int -> IO ()
forall a b. (a -> b) -> a -> b
$! Int -> Set Int -> Set Int
forall a. Ord a => a -> Set a -> Set a
Set.insert Int
n Set Int
s

  writeCommand :: WriterConn t (Writer a) -> Command (Writer a) -> IO ()
writeCommand WriterConn t (Writer a)
conn (SMT2.Cmd cmd) =
    do let cmdout :: Text
cmdout = Text -> Text
Lazy.toStrict (Builder -> Text
Builder.toLazyText Builder
cmd)
       Maybe Text -> OutputStream Text -> IO ()
forall a. Maybe a -> OutputStream a -> IO ()
Streams.write (Text -> Maybe Text
forall a. a -> Maybe a
Just (Text
cmdout Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n")) (WriterConn t (Writer a) -> OutputStream Text
forall t h. WriterConn t h -> OutputStream Text
connHandle WriterConn t (Writer a)
conn)
       -- force a flush
       Maybe Text -> OutputStream Text -> IO ()
forall a. Maybe a -> OutputStream a -> IO ()
Streams.write (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"") (WriterConn t (Writer a) -> OutputStream Text
forall t h. WriterConn t h -> OutputStream Text
connHandle WriterConn t (Writer a)
conn)

-- | Write check sat command
writeCheckSat :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeCheckSat :: WriterConn t (Writer a) -> IO ()
writeCheckSat WriterConn t (Writer a)
w = WriterConn t (Writer a) -> Command (Writer a) -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t (Writer a)
w Command
Command (Writer a)
SMT2.checkSat

writeExit :: forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeExit :: WriterConn t (Writer a) -> IO ()
writeExit WriterConn t (Writer a)
w = (Command -> IO ()) -> Maybe Command -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (WriterConn t (Writer a) -> Command (Writer a) -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t (Writer a)
w) (SMTLib2Tweaks a => Maybe Command
forall a. SMTLib2Tweaks a => Maybe Command
smtlib2exitCommand @a)

setLogic :: SMTLib2Tweaks a => WriterConn t (Writer a) -> SMT2.Logic -> IO ()
setLogic :: WriterConn t (Writer a) -> Logic -> IO ()
setLogic WriterConn t (Writer a)
w Logic
l = WriterConn t (Writer a) -> Command (Writer a) -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t (Writer a)
w (Command (Writer a) -> IO ()) -> Command (Writer a) -> IO ()
forall a b. (a -> b) -> a -> b
$ Logic -> Command
SMT2.setLogic Logic
l

setOption :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Text -> Text -> IO ()
setOption :: WriterConn t (Writer a) -> Text -> Text -> IO ()
setOption WriterConn t (Writer a)
w Text
nm Text
val = WriterConn t (Writer a) -> Command (Writer a) -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t (Writer a)
w (Command (Writer a) -> IO ()) -> Command (Writer a) -> IO ()
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Command
SMT2.setOption Text
nm Text
val

getVersion :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
getVersion :: WriterConn t (Writer a) -> IO ()
getVersion WriterConn t (Writer a)
w = WriterConn t (Writer a) -> Command (Writer a) -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
writeCommand WriterConn t (Writer a)
w (Command (Writer a) -> IO ()) -> Command (Writer a) -> IO ()
forall a b. (a -> b) -> a -> b
$ Command
Command (Writer a)
SMT2.getVersion

getName :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
getName :: WriterConn t (Writer a) -> IO ()
getName WriterConn t (Writer a)
w = WriterConn t (Writer a) -> Command (Writer a) -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
writeCommand WriterConn t (Writer a)
w (Command (Writer a) -> IO ()) -> Command (Writer a) -> IO ()
forall a b. (a -> b) -> a -> b
$ Command
Command (Writer a)
SMT2.getName

-- | Set the produce models option (We typically want this)
setProduceModels :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Bool -> IO ()
setProduceModels :: WriterConn t (Writer a) -> Bool -> IO ()
setProduceModels WriterConn t (Writer a)
w Bool
b = WriterConn t (Writer a) -> Command (Writer a) -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t (Writer a)
w (Command (Writer a) -> IO ()) -> Command (Writer a) -> IO ()
forall a b. (a -> b) -> a -> b
$ Bool -> Command
SMT2.setProduceModels Bool
b

writeGetValue :: SMTLib2Tweaks a => WriterConn t (Writer a) -> [Term] -> IO ()
writeGetValue :: WriterConn t (Writer a) -> [Term] -> IO ()
writeGetValue WriterConn t (Writer a)
w [Term]
l = WriterConn t (Writer a) -> Command (Writer a) -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t (Writer a)
w (Command (Writer a) -> IO ()) -> Command (Writer a) -> IO ()
forall a b. (a -> b) -> a -> b
$ [Term] -> Command
SMT2.getValue [Term]
l

parseBoolSolverValue :: MonadFail m => SExp -> m Bool
parseBoolSolverValue :: SExp -> m Bool
parseBoolSolverValue (SAtom Text
"true")  = Bool -> m Bool
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
True
parseBoolSolverValue (SAtom Text
"false") = Bool -> m Bool
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
False
parseBoolSolverValue SExp
s =
  do BV 1
v <- NatRepr 1 -> SExp -> m (BV 1)
forall (m :: Type -> Type) (w :: Nat).
MonadFail m =>
NatRepr w -> SExp -> m (BV w)
parseBvSolverValue (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) SExp
s
     Bool -> m Bool
forall (m :: Type -> Type) a. Monad m => a -> m a
return (if BV 1
v BV 1 -> BV 1 -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr 1 -> BV 1
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat then Bool
False else Bool
True)

parseRealSolverValue :: MonadFail m => SExp -> m Rational
parseRealSolverValue :: SExp -> m Rational
parseRealSolverValue (SAtom Text
v) | Just (Rational
r,String
"") <- String -> Maybe (Rational, String)
forall (m :: Type -> Type).
MonadFail m =>
String -> m (Rational, String)
readDecimal (Text -> String
Text.unpack Text
v) =
  Rational -> m Rational
forall (m :: Type -> Type) a. Monad m => a -> m a
return Rational
r
parseRealSolverValue (SApp [Item [SExp]
"-", Item [SExp]
x]) = do
  Rational -> Rational
forall a. Num a => a -> a
negate (Rational -> Rational) -> m Rational -> m Rational
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SExp -> m Rational
forall (m :: Type -> Type). MonadFail m => SExp -> m Rational
parseRealSolverValue Item [SExp]
SExp
x
parseRealSolverValue (SApp [Item [SExp]
"/", Item [SExp]
x , Item [SExp]
y]) = do
  Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
(/) (Rational -> Rational -> Rational)
-> m Rational -> m (Rational -> Rational)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SExp -> m Rational
forall (m :: Type -> Type). MonadFail m => SExp -> m Rational
parseRealSolverValue Item [SExp]
SExp
x
      m (Rational -> Rational) -> m Rational -> m Rational
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> SExp -> m Rational
forall (m :: Type -> Type). MonadFail m => SExp -> m Rational
parseRealSolverValue Item [SExp]
SExp
y
parseRealSolverValue SExp
s = String -> m Rational
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> m Rational) -> String -> m Rational
forall a b. (a -> b) -> a -> b
$ String
"Could not parse solver value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExp -> String
forall a. Show a => a -> String
show SExp
s

-- | Parse a bitvector value returned by a solver. Most solvers give
-- results of the right size, but ABC always gives hex results without
-- leading zeros, so they may be larger or smaller than the actual size
-- of the variable.
parseBvSolverValue :: MonadFail m => NatRepr w -> SExp -> m (BV.BV w)
parseBvSolverValue :: NatRepr w -> SExp -> m (BV w)
parseBvSolverValue NatRepr w
w SExp
s
  | Pair NatRepr tp
w' BV tp
bv <- SExp -> Pair NatRepr BV
parseBVLitHelper SExp
s = case NatRepr tp
w' NatRepr tp -> NatRepr w -> NatComparison tp w
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatComparison m n
`compareNat` NatRepr w
w of
      NatLT NatRepr y
zw -> BV w -> m (BV w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr w -> BV tp -> BV w
forall (w :: Nat) (w' :: Nat).
((w + 1) <= w') =>
NatRepr w' -> BV w -> BV w'
BV.zext (NatRepr tp -> NatRepr (y + 1) -> NatRepr (tp + (y + 1))
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr tp
w' (NatRepr y -> NatRepr 1 -> NatRepr (y + 1)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr y
zw NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)) BV tp
bv)
      NatComparison tp w
NatEQ -> BV tp -> m (BV tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return BV tp
bv
      NatGT NatRepr y
_ -> BV w -> m (BV w)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr w -> BV tp -> BV w
forall (w' :: Nat) (w :: Nat).
((w' + 1) <= w) =>
NatRepr w' -> BV w -> BV w'
BV.trunc NatRepr w
w BV tp
bv)

natBV :: Natural
      -- ^ width
      -> Integer
      -- ^ BV value
      -> Pair NatRepr BV.BV
natBV :: Natural -> Integer -> Pair NatRepr BV
natBV Natural
wNatural Integer
x = case Natural -> Some NatRepr
mkNatRepr Natural
wNatural of
  Some NatRepr x
w -> NatRepr x -> BV x -> Pair NatRepr BV
forall k (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair NatRepr x
w (NatRepr x -> Integer -> BV x
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
w Integer
x)

-- | Parse an s-expression and return a bitvector and its width
parseBVLitHelper :: SExp -> Pair NatRepr BV.BV
parseBVLitHelper :: SExp -> Pair NatRepr BV
parseBVLitHelper (SAtom (Text -> String
Text.unpack -> (Char
'#' : Char
'b' : String
n_str))) | [(n, "")] <- ReadS Integer
forall a. Num a => ReadS a
readBin String
n_str =
  Natural -> Integer -> Pair NatRepr BV
natBV (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length String
n_str)) Integer
n
parseBVLitHelper (SAtom (Text -> String
Text.unpack -> (Char
'#' : Char
'x' : String
n_str))) | [(n, "")] <- ReadS Integer
forall a. (Eq a, Num a) => ReadS a
readHex String
n_str =
  Natural -> Integer -> Pair NatRepr BV
natBV (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length String
n_str Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
4)) Integer
n
parseBVLitHelper (SApp [Item [SExp]
"_", SAtom (Text.unpack -> ('b' : 'v' : n_str)), SAtom (Text.unpack -> w_str)])
  | [(n, "")] <- ReadS Integer
forall a. (Eq a, Num a) => ReadS a
readDec String
n_str, [(w, "")] <- ReadS Natural
forall a. (Eq a, Num a) => ReadS a
readDec String
w_str = Natural -> Integer -> Pair NatRepr BV
natBV Natural
w Integer
n
-- BGS: Is this correct?
parseBVLitHelper SExp
_ = Natural -> Integer -> Pair NatRepr BV
natBV Natural
0 Integer
0

parseStringSolverValue :: MonadFail m => SExp -> m ByteString
parseStringSolverValue :: SExp -> m ByteString
parseStringSolverValue (SString Text
t) | Just ByteString
bs <- Text -> Maybe ByteString
unescapeText Text
t = ByteString -> m ByteString
forall (m :: Type -> Type) a. Monad m => a -> m a
return ByteString
bs
parseStringSolverValue SExp
x = String -> m ByteString
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
"Could not parse string solver value:\n  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExp -> String
forall a. Show a => a -> String
show SExp
x)

parseFloatSolverValue :: MonadFail m => FloatPrecisionRepr fpp
                      -> SExp
                      -> m (BV.BV (FloatPrecisionBits fpp))
parseFloatSolverValue :: FloatPrecisionRepr fpp -> SExp -> m (BV (FloatPrecisionBits fpp))
parseFloatSolverValue (FloatingPointPrecisionRepr NatRepr eb
eb NatRepr sb
sb) SExp
s = do
  ParsedFloatResult BV 1
sgn NatRepr eb
eb' BV eb
expt NatRepr sb
sb' BV sb
sig <- SExp -> m ParsedFloatResult
forall (m :: Type -> Type).
MonadFail m =>
SExp -> m ParsedFloatResult
parseFloatLitHelper SExp
s
  case (NatRepr eb
eb NatRepr eb -> NatRepr eb -> Maybe (eb :~: eb)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` NatRepr eb
eb',
        NatRepr sb
sb NatRepr sb -> NatRepr (1 + sb) -> Maybe (sb :~: (1 + sb))
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` ((KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr 1 -> NatRepr sb -> NatRepr (1 + sb)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
`addNat` NatRepr sb
sb')) of
    (Just eb :~: eb
Refl, Just sb :~: (1 + sb)
Refl) -> do
      -- eb' + 1 ~ 1 + eb'
      (eb + 1) :~: (1 + eb)
Refl <- ((eb + 1) :~: (1 + eb)) -> m ((eb + 1) :~: (1 + eb))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (((eb + 1) :~: (1 + eb)) -> m ((eb + 1) :~: (1 + eb)))
-> ((eb + 1) :~: (1 + eb)) -> m ((eb + 1) :~: (1 + eb))
forall a b. (a -> b) -> a -> b
$ NatRepr eb -> NatRepr 1 -> (eb + 1) :~: (1 + eb)
forall (f :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
f m -> g n -> (m + n) :~: (n + m)
plusComm NatRepr eb
eb' (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1)
      -- (eb' + 1) + sb' ~ eb' + (1 + sb') 
      (eb + sb) :~: ((eb + 1) + sb)
Refl <- ((eb + sb) :~: ((eb + 1) + sb))
-> m ((eb + sb) :~: ((eb + 1) + sb))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (((eb + sb) :~: ((eb + 1) + sb))
 -> m ((eb + sb) :~: ((eb + 1) + sb)))
-> ((eb + sb) :~: ((eb + 1) + sb))
-> m ((eb + sb) :~: ((eb + 1) + sb))
forall a b. (a -> b) -> a -> b
$ NatRepr eb
-> NatRepr 1 -> NatRepr sb -> (eb + (1 + sb)) :~: ((eb + 1) + sb)
forall (f :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat)
       (h :: Nat -> Type) (o :: Nat).
f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o)
plusAssoc NatRepr eb
eb' (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr sb
sb'
      BV (eb + sb) -> m (BV (eb + sb))
forall (m :: Type -> Type) a. Monad m => a -> m a
return BV (eb + sb)
BV ((1 + eb) + sb)
bv
        where bv :: BV ((1 + eb) + sb)
bv = NatRepr (1 + eb)
-> NatRepr sb -> BV (1 + eb) -> BV sb -> BV ((1 + eb) + sb)
forall (w :: Nat) (w' :: Nat).
NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
BV.concat (NatRepr 1 -> NatRepr eb -> NatRepr (1 + eb)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr eb
eb) NatRepr sb
sb' (NatRepr 1 -> NatRepr eb -> BV 1 -> BV eb -> BV (1 + eb)
forall (w :: Nat) (w' :: Nat).
NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
BV.concat NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat NatRepr eb
eb BV 1
sgn BV eb
BV eb
expt) BV sb
sig
    (Maybe (eb :~: eb), Maybe (sb :~: (1 + sb)))
_ -> String -> m (BV (eb + sb))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> m (BV (eb + sb))) -> String -> m (BV (eb + sb))
forall a b. (a -> b) -> a -> b
$ String
"Unexpected float precision: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> NatRepr eb -> String
forall a. Show a => a -> String
show NatRepr eb
eb' String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> NatRepr sb -> String
forall a. Show a => a -> String
show NatRepr sb
sb'

data ParsedFloatResult = forall eb sb . ParsedFloatResult
  (BV.BV 1)    -- sign
  (NatRepr eb) -- exponent width
  (BV.BV eb)   -- exponent
  (NatRepr sb) -- significand bit width
  (BV.BV sb)   -- significand bit

parseFloatLitHelper :: MonadFail m => SExp -> m ParsedFloatResult
parseFloatLitHelper :: SExp -> m ParsedFloatResult
parseFloatLitHelper (SApp [Item [SExp]
"fp", Item [SExp]
sign_s, Item [SExp]
expt_s, Item [SExp]
scand_s])
  | Pair NatRepr tp
sign_w BV tp
sign <- SExp -> Pair NatRepr BV
parseBVLitHelper Item [SExp]
SExp
sign_s
  , Just tp :~: 1
Refl <- NatRepr tp
sign_w NatRepr tp -> NatRepr 1 -> Maybe (tp :~: 1)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1)
  , Pair NatRepr tp
eb BV tp
expt <- SExp -> Pair NatRepr BV
parseBVLitHelper Item [SExp]
SExp
expt_s
  , Pair NatRepr tp
sb BV tp
scand <- SExp -> Pair NatRepr BV
parseBVLitHelper Item [SExp]
SExp
scand_s
  = ParsedFloatResult -> m ParsedFloatResult
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ParsedFloatResult -> m ParsedFloatResult)
-> ParsedFloatResult -> m ParsedFloatResult
forall a b. (a -> b) -> a -> b
$ BV 1
-> NatRepr tp -> BV tp -> NatRepr tp -> BV tp -> ParsedFloatResult
forall (eb :: Nat) (sb :: Nat).
BV 1
-> NatRepr eb -> BV eb -> NatRepr sb -> BV sb -> ParsedFloatResult
ParsedFloatResult BV tp
BV 1
sign NatRepr tp
eb BV tp
expt NatRepr tp
sb BV tp
scand
parseFloatLitHelper
  s :: SExp
s@(SApp [Item [SExp]
"_", SAtom (Text.unpack -> nm), SAtom (Text.unpack -> eb_s), SAtom (Text.unpack -> sb_s)])
  | [(eb_n, "")] <- ReadS Natural
forall a. (Eq a, Num a) => ReadS a
readDec String
eb_s, [(sb_n, "")] <- ReadS Natural
forall a. (Eq a, Num a) => ReadS a
readDec String
sb_s
  , Some NatRepr x
eb <- Natural -> Some NatRepr
mkNatRepr Natural
eb_n
  , Some NatRepr x
sb <- Natural -> Some NatRepr
mkNatRepr (Natural
sb_nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
-Natural
1)
  = case String
nm of
      String
"+oo"   -> ParsedFloatResult -> m ParsedFloatResult
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ParsedFloatResult -> m ParsedFloatResult)
-> ParsedFloatResult -> m ParsedFloatResult
forall a b. (a -> b) -> a -> b
$ BV 1 -> NatRepr x -> BV x -> NatRepr x -> BV x -> ParsedFloatResult
forall (eb :: Nat) (sb :: Nat).
BV 1
-> NatRepr eb -> BV eb -> NatRepr sb -> BV sb -> ParsedFloatResult
ParsedFloatResult (NatRepr 1 -> BV 1
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat) NatRepr x
eb (NatRepr x -> BV x
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr x
eb) NatRepr x
sb (NatRepr x -> BV x
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr x
sb)
      String
"-oo"   -> ParsedFloatResult -> m ParsedFloatResult
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ParsedFloatResult -> m ParsedFloatResult)
-> ParsedFloatResult -> m ParsedFloatResult
forall a b. (a -> b) -> a -> b
$ BV 1 -> NatRepr x -> BV x -> NatRepr x -> BV x -> ParsedFloatResult
forall (eb :: Nat) (sb :: Nat).
BV 1
-> NatRepr eb -> BV eb -> NatRepr sb -> BV sb -> ParsedFloatResult
ParsedFloatResult (NatRepr 1 -> BV 1
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.one NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)  NatRepr x
eb (NatRepr x -> BV x
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr x
eb) NatRepr x
sb (NatRepr x -> BV x
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr x
sb)
      String
"+zero" -> ParsedFloatResult -> m ParsedFloatResult
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ParsedFloatResult -> m ParsedFloatResult)
-> ParsedFloatResult -> m ParsedFloatResult
forall a b. (a -> b) -> a -> b
$ BV 1 -> NatRepr x -> BV x -> NatRepr x -> BV x -> ParsedFloatResult
forall (eb :: Nat) (sb :: Nat).
BV 1
-> NatRepr eb -> BV eb -> NatRepr sb -> BV sb -> ParsedFloatResult
ParsedFloatResult (NatRepr 1 -> BV 1
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat) NatRepr x
eb (NatRepr x -> BV x
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr x
eb)        NatRepr x
sb (NatRepr x -> BV x
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr x
sb)
      String
"-zero" -> ParsedFloatResult -> m ParsedFloatResult
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ParsedFloatResult -> m ParsedFloatResult)
-> ParsedFloatResult -> m ParsedFloatResult
forall a b. (a -> b) -> a -> b
$ BV 1 -> NatRepr x -> BV x -> NatRepr x -> BV x -> ParsedFloatResult
forall (eb :: Nat) (sb :: Nat).
BV 1
-> NatRepr eb -> BV eb -> NatRepr sb -> BV sb -> ParsedFloatResult
ParsedFloatResult (NatRepr 1 -> BV 1
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.one NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)  NatRepr x
eb (NatRepr x -> BV x
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr x
eb)        NatRepr x
sb (NatRepr x -> BV x
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr x
sb)
      String
"NaN"   -> ParsedFloatResult -> m ParsedFloatResult
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ParsedFloatResult -> m ParsedFloatResult)
-> ParsedFloatResult -> m ParsedFloatResult
forall a b. (a -> b) -> a -> b
$ BV 1 -> NatRepr x -> BV x -> NatRepr x -> BV x -> ParsedFloatResult
forall (eb :: Nat) (sb :: Nat).
BV 1
-> NatRepr eb -> BV eb -> NatRepr sb -> BV sb -> ParsedFloatResult
ParsedFloatResult (NatRepr 1 -> BV 1
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat) NatRepr x
eb (NatRepr x -> BV x
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr x
eb) NatRepr x
sb (NatRepr x -> BV x
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr x
sb)
      String
_       -> String -> m ParsedFloatResult
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> m ParsedFloatResult) -> String -> m ParsedFloatResult
forall a b. (a -> b) -> a -> b
$ String
"Could not parse float solver value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExp -> String
forall a. Show a => a -> String
show SExp
s
parseFloatLitHelper SExp
s = String -> m ParsedFloatResult
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> m ParsedFloatResult) -> String -> m ParsedFloatResult
forall a b. (a -> b) -> a -> b
$ String
"Could not parse float solver value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExp -> String
forall a. Show a => a -> String
show SExp
s

parseBvArraySolverValue :: (MonadFail m,
                            1 <= w,
                            1 <= v)
                        => NatRepr w
                        -> NatRepr v
                        -> SExp
                        -> m (Maybe (GroundArray (Ctx.SingleCtx (BaseBVType w)) (BaseBVType v)))
parseBvArraySolverValue :: NatRepr w
-> NatRepr v
-> SExp
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
parseBvArraySolverValue NatRepr w
_ NatRepr v
v (SApp [SApp ["as", "const", _], Item [SExp]
c]) = do
  BV v
c' <- NatRepr v -> SExp -> m (BV v)
forall (m :: Type -> Type) (w :: Nat).
MonadFail m =>
NatRepr w -> SExp -> m (BV w)
parseBvSolverValue NatRepr v
v Item [SExp]
SExp
c
  Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
 -> m (Maybe
         (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))))
-> (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)
    -> Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
-> GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)
-> Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
forall a. a -> Maybe a
Just (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)
 -> m (Maybe
         (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))))
-> GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
forall a b. (a -> b) -> a -> b
$ GroundValue (BaseBVType v)
-> Map
     (Assignment IndexLit (SingleCtx (BaseBVType w)))
     (GroundValue (BaseBVType v))
-> GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)
forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete BV v
GroundValue (BaseBVType v)
c' Map
  (Assignment IndexLit (SingleCtx (BaseBVType w)))
  (GroundValue (BaseBVType v))
forall k a. Map k a
Map.empty
parseBvArraySolverValue NatRepr w
w NatRepr v
v (SApp [Item [SExp]
"store", Item [SExp]
arr, Item [SExp]
idx, Item [SExp]
val]) = do
  Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
arr' <- NatRepr w
-> NatRepr v
-> SExp
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
forall (m :: Type -> Type) (w :: Nat) (v :: Nat).
(MonadFail m, 1 <= w, 1 <= v) =>
NatRepr w
-> NatRepr v
-> SExp
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
parseBvArraySolverValue NatRepr w
w NatRepr v
v Item [SExp]
SExp
arr
  case Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
arr' of
    Just (ArrayConcrete GroundValue (BaseBVType v)
base Map
  (Assignment IndexLit (SingleCtx (BaseBVType w)))
  (GroundValue (BaseBVType v))
m) -> do
      IndexLit (BaseBVType w)
idx' <- NatRepr w -> BV w -> IndexLit (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BV w -> IndexLit (BaseBVType w)
B.BVIndexLit NatRepr w
w (BV w -> IndexLit (BaseBVType w))
-> m (BV w) -> m (IndexLit (BaseBVType w))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr w -> SExp -> m (BV w)
forall (m :: Type -> Type) (w :: Nat).
MonadFail m =>
NatRepr w -> SExp -> m (BV w)
parseBvSolverValue NatRepr w
w Item [SExp]
SExp
idx
      BV v
val' <- NatRepr v -> SExp -> m (BV v)
forall (m :: Type -> Type) (w :: Nat).
MonadFail m =>
NatRepr w -> SExp -> m (BV w)
parseBvSolverValue NatRepr v
v Item [SExp]
SExp
val
      Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
 -> m (Maybe
         (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))))
-> (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)
    -> Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
-> GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)
-> Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
forall a. a -> Maybe a
Just (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)
 -> m (Maybe
         (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))))
-> GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
forall a b. (a -> b) -> a -> b
$ GroundValue (BaseBVType v)
-> Map
     (Assignment IndexLit (SingleCtx (BaseBVType w)))
     (GroundValue (BaseBVType v))
-> GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)
forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete GroundValue (BaseBVType v)
base (Assignment IndexLit (SingleCtx (BaseBVType w))
-> BV v
-> Map (Assignment IndexLit (SingleCtx (BaseBVType w))) (BV v)
-> Map (Assignment IndexLit (SingleCtx (BaseBVType w))) (BV v)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Assignment IndexLit EmptyCtx
forall k (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty Assignment IndexLit EmptyCtx
-> IndexLit (BaseBVType w)
-> Assignment IndexLit (SingleCtx (BaseBVType w))
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> IndexLit (BaseBVType w)
idx') BV v
val' Map (Assignment IndexLit (SingleCtx (BaseBVType w))) (BV v)
Map
  (Assignment IndexLit (SingleCtx (BaseBVType w)))
  (GroundValue (BaseBVType v))
m)
    Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
_ -> Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
forall a. Maybe a
Nothing
parseBvArraySolverValue NatRepr w
_ NatRepr v
_ SExp
_ = Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
forall a. Maybe a
Nothing

------------------------------------------------------------------------
-- Session

-- | This is an interactive session with an SMT solver
data Session t a = Session
  { Session t a -> WriterConn t (Writer a)
sessionWriter   :: !(WriterConn t (Writer a))
  , Session t a -> InputStream Text
sessionResponse :: !(Streams.InputStream Text)
  }

parseSMTLib2String :: AT.Parser Text
parseSMTLib2String :: Parser Text
parseSMTLib2String = Char -> Parser Char
AT.char Char
'\"' Parser Char -> Parser Text -> Parser Text
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Parser Text
go
 where
 go :: AT.Parser Text
 go :: Parser Text
go = do Text
xs <- (Char -> Bool) -> Parser Text
AT.takeWhile (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
'\"'))
         Char
_ <- Char -> Parser Char
AT.char Char
'\"'
         (do Char
_ <- Char -> Parser Char
AT.char Char
'\"'
             Text
ys <- Parser Text
go
             Text -> Parser Text
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text
xs Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\"" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ys)
          ) Parser Text -> Parser Text -> Parser Text
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text
forall (m :: Type -> Type) a. Monad m => a -> m a
return Text
xs

-- | Get a value from a solver (must be called after checkSat)
runGetValue :: SMTLib2Tweaks a
            => Session t a
            -> Term
            -> IO SExp
runGetValue :: Session t a -> Term -> IO SExp
runGetValue Session t a
s Term
e = do
  WriterConn t (Writer a) -> [Term] -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> [Term] -> IO ()
writeGetValue (Session t a -> WriterConn t (Writer a)
forall t a. Session t a -> WriterConn t (Writer a)
sessionWriter Session t a
s) [ Item [Term]
Term
e ]
  Either ParseException SExp
msexp <- IO SExp -> IO (Either ParseException SExp)
forall e a. Exception e => IO a -> IO (Either e a)
try (IO SExp -> IO (Either ParseException SExp))
-> IO SExp -> IO (Either ParseException SExp)
forall a b. (a -> b) -> a -> b
$ Parser SExp -> InputStream Text -> IO SExp
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseSMTLib2String) (Session t a -> InputStream Text
forall t a. Session t a -> InputStream Text
sessionResponse Session t a
s)
  case Either ParseException SExp
msexp of
    Left Streams.ParseException{} -> String -> IO SExp
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO SExp) -> String -> IO SExp
forall a b. (a -> b) -> a -> b
$ String
"Could not parse solver value."
    Right (SApp [SApp [_, b]]) -> SExp -> IO SExp
forall (m :: Type -> Type) a. Monad m => a -> m a
return Item [SExp]
SExp
b
    Right SExp
sexp -> String -> IO SExp
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO SExp) -> String -> IO SExp
forall a b. (a -> b) -> a -> b
$ String
"Could not parse solver value:\n  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExp -> String
forall a. Show a => a -> String
show SExp
sexp

-- | This function runs a check sat command
runCheckSat :: forall b t a.
               SMTLib2Tweaks b
            => Session t b
            -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
               -- ^ Function for evaluating model.
               -- The evaluation should be complete before
            -> IO a
runCheckSat :: Session t b
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runCheckSat Session t b
s SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
doEval =
  do let w :: WriterConn t (Writer b)
w = Session t b -> WriterConn t (Writer b)
forall t a. Session t a -> WriterConn t (Writer a)
sessionWriter Session t b
s
         r :: InputStream Text
r = Session t b -> InputStream Text
forall t a. Session t a -> InputStream Text
sessionResponse Session t b
s
     WriterConn t (Writer b) -> [Command (Writer b)] -> IO ()
forall h t. SMTWriter h => WriterConn t h -> [Command h] -> IO ()
addCommands WriterConn t (Writer b)
w (WriterConn t (Writer b) -> [Command (Writer b)]
forall h (f :: Type -> Type). SMTWriter h => f h -> [Command h]
checkCommands WriterConn t (Writer b)
w)
     SatResult () ()
res <- WriterConn t (Writer b) -> InputStream Text -> IO (SatResult () ())
forall h (f :: Type -> Type).
SMTReadWriter h =>
f h -> InputStream Text -> IO (SatResult () ())
smtSatResult WriterConn t (Writer b)
w InputStream Text
r
     case SatResult () ()
res of
       Unsat ()
x -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
doEval (() -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
forall mdl core. core -> SatResult mdl core
Unsat ()
x)
       SatResult () ()
Unknown -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
doEval SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
forall mdl core. SatResult mdl core
Unknown
       Sat ()
_ ->
         do GroundEvalFn t
evalFn <- WriterConn t (Writer b)
-> SMTEvalFunctions (Writer b) -> IO (GroundEvalFn t)
forall t h.
SMTWriter h =>
WriterConn t h -> SMTEvalFunctions h -> IO (GroundEvalFn t)
smtExprGroundEvalFn WriterConn t (Writer b)
w (WriterConn t (Writer b)
-> InputStream Text -> SMTEvalFunctions (Writer b)
forall h t.
SMTReadWriter h =>
WriterConn t h -> InputStream Text -> SMTEvalFunctions h
smtEvalFuns WriterConn t (Writer b)
w InputStream Text
r)
            SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
doEval ((GroundEvalFn t, Maybe (ExprRangeBindings t))
-> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
forall mdl core. mdl -> SatResult mdl core
Sat (GroundEvalFn t
evalFn, Maybe (ExprRangeBindings t)
forall a. Maybe a
Nothing))

-- | Called when methods in the following instance encounter an exception
throwSMTLib2ParseError :: (Exception e) => Text -> SMT2.Command -> e -> m a
throwSMTLib2ParseError :: Text -> Command -> e -> m a
throwSMTLib2ParseError Text
what Command
cmd e
e =
  SMTLib2Exception -> m a
forall a e. Exception e => e -> a
throw (SMTLib2Exception -> m a) -> SMTLib2Exception -> m a
forall a b. (a -> b) -> a -> b
$ [Command] -> Text -> SMTLib2Exception
SMTLib2ParseError [Item [Command]
Command
cmd] (Text -> SMTLib2Exception) -> Text -> SMTLib2Exception
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
Text.unlines
    [ [Text] -> Text
Text.unwords [Item [Text]
"Could not parse result from", Text
Item [Text]
what, Item [Text]
"."]
    , Text
"*** Exception: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
Text.pack (e -> String
forall e. Exception e => e -> String
displayException e
e)
    ]

instance SMTLib2Tweaks a => SMTReadWriter (Writer a) where
  smtEvalFuns :: WriterConn t (Writer a)
-> InputStream Text -> SMTEvalFunctions (Writer a)
smtEvalFuns WriterConn t (Writer a)
w InputStream Text
s = Session t a -> SMTEvalFunctions (Writer a)
forall t a.
SMTLib2Tweaks a =>
Session t a -> SMTEvalFunctions (Writer a)
smtLibEvalFuns Session :: forall t a.
WriterConn t (Writer a) -> InputStream Text -> Session t a
Session { sessionWriter :: WriterConn t (Writer a)
sessionWriter = WriterConn t (Writer a)
w
                                           , sessionResponse :: InputStream Text
sessionResponse = InputStream Text
s }

  smtSatResult :: f (Writer a) -> InputStream Text -> IO (SatResult () ())
smtSatResult f (Writer a)
p InputStream Text
s =
    do Either SomeException SExp
mb <- (SomeException -> Maybe SomeException)
-> IO SExp -> IO (Either SomeException SExp)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (Parser SExp -> InputStream Text -> IO SExp
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseSMTLib2String) InputStream Text
s)
       case Either SomeException SExp
mb of
         Left (SomeException e
e) ->
            String -> IO (SatResult () ())
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (SatResult () ())) -> String -> IO (SatResult () ())
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ Item [String]
"Could not parse check_sat result."
                           , String
"*** Exception: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ e -> String
forall e. Exception e => e -> String
displayException e
e
                           ]
         Right (SAtom Text
"unsat") -> SatResult () () -> IO (SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return (() -> SatResult () ()
forall mdl core. core -> SatResult mdl core
Unsat ())
         Right (SAtom Text
"sat") -> SatResult () () -> IO (SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return (() -> SatResult () ()
forall mdl core. mdl -> SatResult mdl core
Sat ())
         Right (SAtom Text
"unknown") -> SatResult () () -> IO (SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult () ()
forall mdl core. SatResult mdl core
Unknown
         Right (SApp [SAtom "error", SString msg]) -> SMTLib2Exception -> IO (SatResult () ())
forall a e. Exception e => e -> a
throw (Command -> Text -> SMTLib2Exception
SMTLib2Error ([Command] -> Command
forall a. [a] -> a
head ([Command] -> Command) -> [Command] -> Command
forall a b. (a -> b) -> a -> b
$ [Command] -> [Command]
forall a. [a] -> [a]
reverse (f (Writer a) -> [Command (Writer a)]
forall h (f :: Type -> Type). SMTWriter h => f h -> [Command h]
checkCommands f (Writer a)
p)) Text
msg)
         Right SExp
res -> SMTLib2Exception -> IO (SatResult () ())
forall a e. Exception e => e -> a
throw (SMTLib2Exception -> IO (SatResult () ()))
-> SMTLib2Exception -> IO (SatResult () ())
forall a b. (a -> b) -> a -> b
$ [Command] -> Text -> SMTLib2Exception
SMTLib2ParseError (f (Writer a) -> [Command (Writer a)]
forall h (f :: Type -> Type). SMTWriter h => f h -> [Command h]
checkCommands f (Writer a)
p) (String -> Text
Text.pack (SExp -> String
forall a. Show a => a -> String
show SExp
res))

  smtUnsatAssumptionsResult :: f (Writer a) -> InputStream Text -> IO [(Bool, Text)]
smtUnsatAssumptionsResult f (Writer a)
p InputStream Text
s =
    do Either SomeException SExp
mb <- (SomeException -> Maybe SomeException)
-> IO SExp -> IO (Either SomeException SExp)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (Parser SExp -> InputStream Text -> IO SExp
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseSMTLib2String) InputStream Text
s)
       let cmd :: Command (Writer a)
cmd = f (Writer a) -> Command (Writer a)
forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
getUnsatAssumptionsCommand f (Writer a)
p
       case Either SomeException SExp
mb of
         Right (SExp -> Maybe [(Bool, Text)]
asNegAtomList -> Just [(Bool, Text)]
as) -> [(Bool, Text)] -> IO [(Bool, Text)]
forall (m :: Type -> Type) a. Monad m => a -> m a
return [(Bool, Text)]
as
         Right (SApp [SAtom "error", SString msg]) -> SMTLib2Exception -> IO [(Bool, Text)]
forall a e. Exception e => e -> a
throw (Command -> Text -> SMTLib2Exception
SMTLib2Error Command
Command (Writer a)
cmd Text
msg)
         Right SExp
res -> SMTLib2Exception -> IO [(Bool, Text)]
forall a e. Exception e => e -> a
throw ([Command] -> Text -> SMTLib2Exception
SMTLib2ParseError [Item [Command]
Command (Writer a)
cmd] (String -> Text
Text.pack (SExp -> String
forall a. Show a => a -> String
show SExp
res)))
         Left (SomeException e
e) ->
           Text -> Command -> e -> IO [(Bool, Text)]
forall e (m :: Type -> Type) a.
Exception e =>
Text -> Command -> e -> m a
throwSMTLib2ParseError Text
"unsat assumptions" Command
Command (Writer a)
cmd e
e

  smtUnsatCoreResult :: f (Writer a) -> InputStream Text -> IO [Text]
smtUnsatCoreResult f (Writer a)
p InputStream Text
s =
    do Either SomeException SExp
mb <- (SomeException -> Maybe SomeException)
-> IO SExp -> IO (Either SomeException SExp)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (Parser SExp -> InputStream Text -> IO SExp
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseSMTLib2String) InputStream Text
s)
       let cmd :: Command (Writer a)
cmd = f (Writer a) -> Command (Writer a)
forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
getUnsatCoreCommand f (Writer a)
p
       case Either SomeException SExp
mb of
         Right (SExp -> Maybe [Text]
asAtomList -> Just [Text]
nms) -> [Text] -> IO [Text]
forall (m :: Type -> Type) a. Monad m => a -> m a
return [Text]
nms
         Right (SApp [SAtom "error", SString msg]) -> SMTLib2Exception -> IO [Text]
forall a e. Exception e => e -> a
throw (Command -> Text -> SMTLib2Exception
SMTLib2Error Command
Command (Writer a)
cmd Text
msg)
         Right SExp
res -> SMTLib2Exception -> IO [Text]
forall a e. Exception e => e -> a
throw ([Command] -> Text -> SMTLib2Exception
SMTLib2ParseError [Item [Command]
Command (Writer a)
cmd] (String -> Text
Text.pack (SExp -> String
forall a. Show a => a -> String
show SExp
res)))
         Left (SomeException e
e) ->
           Text -> Command -> e -> IO [Text]
forall e (m :: Type -> Type) a.
Exception e =>
Text -> Command -> e -> m a
throwSMTLib2ParseError Text
"unsat core" Command
Command (Writer a)
cmd e
e


data SMTLib2Exception
  = SMTLib2Unsupported SMT2.Command
  | SMTLib2Error SMT2.Command Text
  | SMTLib2ParseError [SMT2.Command] Text

instance Show SMTLib2Exception where
  show :: SMTLib2Exception -> String
show (SMTLib2Unsupported (SMT2.Cmd Builder
cmd)) =
     [String] -> String
unlines
       [ Item [String]
"unsupported command:"
       , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
Lazy.unpack (Builder -> Text
Builder.toLazyText Builder
cmd)
       ]
  show (SMTLib2Error (SMT2.Cmd Builder
cmd) Text
msg) =
     [String] -> String
unlines
       [ Item [String]
"Solver reported an error:"
       , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack Text
msg
       , Item [String]
"in response to command:"
       , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
Lazy.unpack (Builder -> Text
Builder.toLazyText Builder
cmd)
       ]
  show (SMTLib2ParseError [Command]
cmds Text
msg) =
     [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
       [ Item [String]
"Could not parse solver response:"
       , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack Text
msg
       , Item [String]
"in response to commands:"
       ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Command -> String) -> [Command] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Command -> String
cmdToString [Command]
cmds
       where cmdToString :: Command -> String
cmdToString (SMT2.Cmd Builder
cmd) =
               String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
Lazy.unpack (Builder -> Text
Builder.toLazyText Builder
cmd)

instance Exception SMTLib2Exception

smtAckResult :: AcknowledgementAction t (Writer a)
smtAckResult :: AcknowledgementAction t (Writer a)
smtAckResult = (WriterConn t (Writer a) -> Command (Writer a) -> IO ())
-> AcknowledgementAction t (Writer a)
forall t h.
(WriterConn t h -> Command h -> IO ()) -> AcknowledgementAction t h
AckAction ((WriterConn t (Writer a) -> Command (Writer a) -> IO ())
 -> AcknowledgementAction t (Writer a))
-> (WriterConn t (Writer a) -> Command (Writer a) -> IO ())
-> AcknowledgementAction t (Writer a)
forall a b. (a -> b) -> a -> b
$ \WriterConn t (Writer a)
conn Command (Writer a)
cmd ->
  do Either SomeException SExp
mb <- (SomeException -> Maybe SomeException)
-> IO SExp -> IO (Either SomeException SExp)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (Parser SExp -> InputStream Text -> IO SExp
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseSMTLib2String) (WriterConn t (Writer a) -> InputStream Text
forall t h. WriterConn t h -> InputStream Text
connInputHandle WriterConn t (Writer a)
conn))
     case Either SomeException SExp
mb of
       Right (SAtom Text
"success") -> () -> IO ()
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
       Right (SAtom Text
"unsupported") -> SMTLib2Exception -> IO ()
forall a e. Exception e => e -> a
throw (Command -> SMTLib2Exception
SMTLib2Unsupported Command
Command (Writer a)
cmd)
       Right (SApp [SAtom "error", SString msg]) -> SMTLib2Exception -> IO ()
forall a e. Exception e => e -> a
throw (Command -> Text -> SMTLib2Exception
SMTLib2Error Command
Command (Writer a)
cmd Text
msg)
       Right SExp
res -> SMTLib2Exception -> IO ()
forall a e. Exception e => e -> a
throw ([Command] -> Text -> SMTLib2Exception
SMTLib2ParseError [Item [Command]
Command (Writer a)
cmd] (String -> Text
Text.pack (SExp -> String
forall a. Show a => a -> String
show SExp
res)))
       Left (SomeException e
e) -> SMTLib2Exception -> IO ()
forall a e. Exception e => e -> a
throw (SMTLib2Exception -> IO ()) -> SMTLib2Exception -> IO ()
forall a b. (a -> b) -> a -> b
$ [Command] -> Text -> SMTLib2Exception
SMTLib2ParseError [Item [Command]
Command (Writer a)
cmd] (Text -> SMTLib2Exception) -> Text -> SMTLib2Exception
forall a b. (a -> b) -> a -> b
$ String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$
               [String] -> String
unlines [ Item [String]
"Could not parse acknowledgement result."
                       , String
"*** Exception: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ e -> String
forall e. Exception e => e -> String
displayException e
e
                       ]

smtLibEvalFuns ::
  forall t a. SMTLib2Tweaks a => Session t a -> SMTEvalFunctions (Writer a)
smtLibEvalFuns :: Session t a -> SMTEvalFunctions (Writer a)
smtLibEvalFuns Session t a
s = SMTEvalFunctions :: forall h.
(Term h -> IO Bool)
-> (forall (w :: Nat). NatRepr w -> Term h -> IO (BV w))
-> (Term h -> IO Rational)
-> (forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp
    -> Term h -> IO (BV (FloatPrecisionBits fpp)))
-> Maybe (SMTEvalBVArrayWrapper h)
-> (Term h -> IO ByteString)
-> SMTEvalFunctions h
SMTEvalFunctions
                  { smtEvalBool :: Term (Writer a) -> IO Bool
smtEvalBool = Term -> IO Bool
Term (Writer a) -> IO Bool
evalBool
                  , smtEvalBV :: forall (w :: Nat). NatRepr w -> Term (Writer a) -> IO (BV w)
smtEvalBV = forall (w :: Nat). NatRepr w -> Term -> IO (BV w)
forall (w :: Nat). NatRepr w -> Term (Writer a) -> IO (BV w)
evalBV
                  , smtEvalReal :: Term (Writer a) -> IO Rational
smtEvalReal = Term -> IO Rational
Term (Writer a) -> IO Rational
evalReal
                  , smtEvalFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp
-> Term (Writer a) -> IO (BV (FloatPrecisionBits fpp))
smtEvalFloat = forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> Term -> IO (BV (FloatPrecisionBits fpp))
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp
-> Term (Writer a) -> IO (BV (FloatPrecisionBits fpp))
evalFloat
                  , smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper (Writer a))
smtEvalBvArray = SMTEvalBVArrayWrapper (Writer a)
-> Maybe (SMTEvalBVArrayWrapper (Writer a))
forall a. a -> Maybe a
Just ((forall (w :: Nat) (v :: Nat). SMTEvalBVArrayFn (Writer a) w v)
-> SMTEvalBVArrayWrapper (Writer a)
forall h.
(forall (w :: Nat) (v :: Nat). SMTEvalBVArrayFn h w v)
-> SMTEvalBVArrayWrapper h
SMTEvalBVArrayWrapper forall (w :: Nat) (v :: Nat). SMTEvalBVArrayFn (Writer a) w v
evalBvArray)
                  , smtEvalString :: Term (Writer a) -> IO ByteString
smtEvalString = Term -> IO ByteString
Term (Writer a) -> IO ByteString
evalStr
                  }
  where
  evalBool :: Term -> IO Bool
evalBool Term
tm = SExp -> IO Bool
forall (m :: Type -> Type). MonadFail m => SExp -> m Bool
parseBoolSolverValue (SExp -> IO Bool) -> IO SExp -> IO Bool
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Session t a -> Term -> IO SExp
forall a t. SMTLib2Tweaks a => Session t a -> Term -> IO SExp
runGetValue Session t a
s Term
tm
  evalReal :: Term -> IO Rational
evalReal Term
tm = SExp -> IO Rational
forall (m :: Type -> Type). MonadFail m => SExp -> m Rational
parseRealSolverValue (SExp -> IO Rational) -> IO SExp -> IO Rational
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Session t a -> Term -> IO SExp
forall a t. SMTLib2Tweaks a => Session t a -> Term -> IO SExp
runGetValue Session t a
s Term
tm
  evalStr :: Term -> IO ByteString
evalStr Term
tm = SExp -> IO ByteString
forall (m :: Type -> Type). MonadFail m => SExp -> m ByteString
parseStringSolverValue (SExp -> IO ByteString) -> IO SExp -> IO ByteString
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Session t a -> Term -> IO SExp
forall a t. SMTLib2Tweaks a => Session t a -> Term -> IO SExp
runGetValue Session t a
s Term
tm

  evalBV :: NatRepr w -> Term -> IO (BV.BV w)
  evalBV :: NatRepr w -> Term -> IO (BV w)
evalBV NatRepr w
w Term
tm = NatRepr w -> SExp -> IO (BV w)
forall (m :: Type -> Type) (w :: Nat).
MonadFail m =>
NatRepr w -> SExp -> m (BV w)
parseBvSolverValue NatRepr w
w (SExp -> IO (BV w)) -> IO SExp -> IO (BV w)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Session t a -> Term -> IO SExp
forall a t. SMTLib2Tweaks a => Session t a -> Term -> IO SExp
runGetValue Session t a
s Term
tm

  evalFloat :: FloatPrecisionRepr fpp -> Term -> IO (BV.BV (FloatPrecisionBits fpp))
  evalFloat :: FloatPrecisionRepr fpp -> Term -> IO (BV (FloatPrecisionBits fpp))
evalFloat FloatPrecisionRepr fpp
fpp Term
tm = FloatPrecisionRepr fpp -> SExp -> IO (BV (FloatPrecisionBits fpp))
forall (m :: Type -> Type) (fpp :: FloatPrecision).
MonadFail m =>
FloatPrecisionRepr fpp -> SExp -> m (BV (FloatPrecisionBits fpp))
parseFloatSolverValue FloatPrecisionRepr fpp
fpp (SExp -> IO (BV (FloatPrecisionBits fpp)))
-> IO SExp -> IO (BV (FloatPrecisionBits fpp))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Session t a -> Term -> IO SExp
forall a t. SMTLib2Tweaks a => Session t a -> Term -> IO SExp
runGetValue Session t a
s Term
tm

  evalBvArray :: SMTEvalBVArrayFn (Writer a) w v
  evalBvArray :: NatRepr w
-> NatRepr v
-> Term (Writer a)
-> IO
     (Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
evalBvArray NatRepr w
w NatRepr v
v Term (Writer a)
tm = NatRepr w
-> NatRepr v
-> SExp
-> IO
     (Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
forall (m :: Type -> Type) (w :: Nat) (v :: Nat).
(MonadFail m, 1 <= w, 1 <= v) =>
NatRepr w
-> NatRepr v
-> SExp
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
parseBvArraySolverValue NatRepr w
w NatRepr v
v (SExp
 -> IO
      (Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))))
-> IO SExp
-> IO
     (Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Session t a -> Term -> IO SExp
forall a t. SMTLib2Tweaks a => Session t a -> Term -> IO SExp
runGetValue Session t a
s Term
Term (Writer a)
tm


class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where
  defaultSolverPath :: a -> B.ExprBuilder t st fs -> IO FilePath

  defaultSolverArgs :: a -> B.ExprBuilder t st fs -> IO [String]

  defaultFeatures :: a -> ProblemFeatures

  getErrorBehavior :: a -> WriterConn t (Writer a) -> Streams.InputStream Text -> IO ErrorBehavior
  getErrorBehavior a
_ WriterConn t (Writer a)
_ InputStream Text
_ = ErrorBehavior -> IO ErrorBehavior
forall (m :: Type -> Type) a. Monad m => a -> m a
return ErrorBehavior
ImmediateExit

  supportsResetAssertions :: a -> Bool
  supportsResetAssertions a
_ = Bool
False

  setDefaultLogicAndOptions :: WriterConn t (Writer a) -> IO()

  newDefaultWriter
    :: a ->
       AcknowledgementAction t (Writer a) ->
       ProblemFeatures ->
       B.ExprBuilder t st fs ->
       Streams.OutputStream Text ->
       Streams.InputStream Text ->
       IO (WriterConn t (Writer a))
  newDefaultWriter a
solver AcknowledgementAction t (Writer a)
ack ProblemFeatures
feats ExprBuilder t st fs
sym OutputStream Text
h InputStream Text
in_h =
    a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
forall a t.
a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
newWriter a
solver OutputStream Text
h InputStream Text
in_h AcknowledgementAction t (Writer a)
ack (a -> String
forall a. Show a => a -> String
show a
solver) Bool
True ProblemFeatures
feats Bool
True
      (SymbolVarBimap t -> IO (WriterConn t (Writer a)))
-> IO (SymbolVarBimap t) -> IO (WriterConn t (Writer a))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs -> IO (SymbolVarBimap t)
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO (SymbolVarBimap t)
B.getSymbolVarBimap ExprBuilder t st fs
sym

  -- | Run the solver in a session.
  withSolver
    :: a
    -> AcknowledgementAction t (Writer a)
    -> ProblemFeatures
    -> B.ExprBuilder t st fs
    -> FilePath
      -- ^ Path to solver executable
    -> LogData
    -> (Session t a -> IO b)
      -- ^ Action to run
    -> IO b
  withSolver a
solver AcknowledgementAction t (Writer a)
ack ProblemFeatures
feats ExprBuilder t st fs
sym String
path LogData
logData Session t a -> IO b
action = do
    [String]
args <- a -> ExprBuilder t st fs -> IO [String]
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs a
solver ExprBuilder t st fs
sym
    String
-> [String]
-> Maybe String
-> ((Handle, Handle, Handle, ProcessHandle) -> IO b)
-> IO b
forall a.
String
-> [String]
-> Maybe String
-> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
-> IO a
withProcessHandles String
path [String]
args Maybe String
forall a. Maybe a
Nothing (((Handle, Handle, Handle, ProcessHandle) -> IO b) -> IO b)
-> ((Handle, Handle, Handle, ProcessHandle) -> IO b) -> IO b
forall a b. (a -> b) -> a -> b
$
      \hdls :: (Handle, Handle, Handle, ProcessHandle)
hdls@(Handle
in_h, Handle
out_h, Handle
err_h, ProcessHandle
_ph) -> do

        (OutputStream Text
in_stream, InputStream Text
out_stream, HandleReader
err_reader) <-
          Handle
-> Handle
-> Handle
-> Maybe (Text, Handle)
-> IO (OutputStream Text, InputStream Text, HandleReader)
demuxProcessHandles Handle
in_h Handle
out_h Handle
err_h
            ((Handle -> (Text, Handle)) -> Maybe Handle -> Maybe (Text, Handle)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Handle
x -> (Text
"; ", Handle
x)) (Maybe Handle -> Maybe (Text, Handle))
-> Maybe Handle -> Maybe (Text, Handle)
forall a b. (a -> b) -> a -> b
$ LogData -> Maybe Handle
logHandle LogData
logData)

        WriterConn t (Writer a)
writer <- a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> ExprBuilder t st fs
-> OutputStream Text
-> InputStream Text
-> IO (WriterConn t (Writer a))
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> ExprBuilder t st fs
-> OutputStream Text
-> InputStream Text
-> IO (WriterConn t (Writer a))
newDefaultWriter a
solver AcknowledgementAction t (Writer a)
ack ProblemFeatures
feats ExprBuilder t st fs
sym OutputStream Text
in_stream InputStream Text
out_stream
        let s :: Session t a
s = Session :: forall t a.
WriterConn t (Writer a) -> InputStream Text -> Session t a
Session
              { sessionWriter :: WriterConn t (Writer a)
sessionWriter   = WriterConn t (Writer a)
writer
              , sessionResponse :: InputStream Text
sessionResponse = InputStream Text
out_stream
              }

        -- Set solver logic and solver-specific options
        WriterConn t (Writer a) -> IO ()
forall a t.
SMTLib2GenericSolver a =>
WriterConn t (Writer a) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer a)
writer

        -- Run action with session.
        b
r <- Session t a -> IO b
action Session t a
s
        -- Tell solver to exit
        WriterConn t (Writer a) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeExit WriterConn t (Writer a)
writer

        HandleReader -> IO ()
stopHandleReader HandleReader
err_reader

        ExitCode
ec <- (Handle, Handle, Handle, ProcessHandle) -> IO ExitCode
cleanupProcess (Handle, Handle, Handle, ProcessHandle)
hdls
        case ExitCode
ec of
          ExitCode
Exit.ExitSuccess -> b -> IO b
forall (m :: Type -> Type) a. Monad m => a -> m a
return b
r
          Exit.ExitFailure Int
exit_code -> String -> IO b
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO b) -> String -> IO b
forall a b. (a -> b) -> a -> b
$
            a -> String
forall a. Show a => a -> String
show a
solver String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" exited with unexpected code: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
exit_code

  runSolverInOverride
    :: a
    -> AcknowledgementAction t (Writer a)
    -> ProblemFeatures
    -> B.ExprBuilder t st fs
    -> LogData
    -> [B.BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b)
    -> IO b
  runSolverInOverride a
solver AcknowledgementAction t (Writer a)
ack ProblemFeatures
feats ExprBuilder t st fs
sym LogData
logData [BoolExpr t]
predicates SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b
cont = do
    ExprBuilder t st fs -> SolverEvent -> IO ()
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
I.logSolverEvent ExprBuilder t st fs
sym
      SolverStartSATQuery :: String -> String -> SolverEvent
I.SolverStartSATQuery
        { satQuerySolverName :: String
I.satQuerySolverName = a -> String
forall a. Show a => a -> String
show a
solver
        , satQueryReason :: String
I.satQueryReason     = LogData -> String
logReason LogData
logData
        }
    String
path <- a -> ExprBuilder t st fs -> IO String
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a -> ExprBuilder t st fs -> IO String
defaultSolverPath a
solver ExprBuilder t st fs
sym
    a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t a -> IO b)
-> IO b
forall a t (st :: Type -> Type) fs b.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t a -> IO b)
-> IO b
withSolver a
solver AcknowledgementAction t (Writer a)
ack ProblemFeatures
feats ExprBuilder t st fs
sym String
path (LogData
logData{logVerbosity :: Int
logVerbosity=Int
2}) ((Session t a -> IO b) -> IO b) -> (Session t a -> IO b) -> IO b
forall a b. (a -> b) -> a -> b
$ \Session t a
session -> do
      -- Assume the predicates hold.
      [BoolExpr t] -> (BoolExpr t -> IO ()) -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [BoolExpr t]
predicates (WriterConn t (Writer a) -> BoolExpr t -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMTWriter.assume (Session t a -> WriterConn t (Writer a)
forall t a. Session t a -> WriterConn t (Writer a)
sessionWriter Session t a
session))
      -- Run check SAT and get the model back.
      Session t a
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO b)
-> IO b
forall b t a.
SMTLib2Tweaks b =>
Session t b
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runCheckSat Session t a
session ((SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
  -> IO b)
 -> IO b)
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO b)
-> IO b
forall a b. (a -> b) -> a -> b
$ \SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
result -> do
        ExprBuilder t st fs -> SolverEvent -> IO ()
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
I.logSolverEvent ExprBuilder t st fs
sym
          SolverEndSATQuery :: SatResult () () -> Maybe String -> SolverEvent
I.SolverEndSATQuery
            { satQueryResult :: SatResult () ()
I.satQueryResult = SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
-> SatResult () ()
forall a b. SatResult a b -> SatResult () ()
forgetModelAndCore SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
result
            , satQueryError :: Maybe String
I.satQueryError  = Maybe String
forall a. Maybe a
Nothing
            }
        SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b
cont SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
result

-- | A default method for writing SMTLib2 problems without any
--   solver-specific tweaks.
writeDefaultSMT2 :: SMTLib2Tweaks a
                 => a
                 -> String
                    -- ^ Name of solver for reporting.
                 -> ProblemFeatures
                    -- ^ Features supported by solver
                 -> B.ExprBuilder t st fs
                 -> IO.Handle
                 -> [B.BoolExpr t]
                 -> IO ()
writeDefaultSMT2 :: a
-> String
-> ProblemFeatures
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
writeDefaultSMT2 a
a String
nm ProblemFeatures
feat ExprBuilder t st fs
sym Handle
h [BoolExpr t]
ps = do
  SymbolVarBimap t
bindings <- ExprBuilder t st fs -> IO (SymbolVarBimap t)
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO (SymbolVarBimap t)
B.getSymbolVarBimap ExprBuilder t st fs
sym
  OutputStream Text
str <- OutputStream ByteString -> IO (OutputStream Text)
Streams.encodeUtf8 (OutputStream ByteString -> IO (OutputStream Text))
-> IO (OutputStream ByteString) -> IO (OutputStream Text)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Handle -> IO (OutputStream ByteString)
Streams.handleToOutputStream Handle
h
  InputStream Text
null_in <- IO (InputStream Text)
forall a. IO (InputStream a)
Streams.nullInput
  WriterConn t (Writer a)
c <- a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
forall a t.
a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
newWriter a
a OutputStream Text
str InputStream Text
null_in AcknowledgementAction t (Writer a)
forall t h. AcknowledgementAction t h
nullAcknowledgementAction String
nm Bool
True ProblemFeatures
feat Bool
True SymbolVarBimap t
bindings
  WriterConn t (Writer a) -> Bool -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
setProduceModels WriterConn t (Writer a)
c Bool
True
  [BoolExpr t] -> (BoolExpr t -> IO ()) -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [BoolExpr t]
ps (WriterConn t (Writer a) -> BoolExpr t -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMTWriter.assume WriterConn t (Writer a)
c)
  WriterConn t (Writer a) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeCheckSat WriterConn t (Writer a)
c
  WriterConn t (Writer a) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeExit WriterConn t (Writer a)
c

startSolver
  :: SMTLib2GenericSolver a
  => a
  -> AcknowledgementAction t (Writer a)
        -- ^ Action for acknowledging command responses
  -> (WriterConn t (Writer a) -> IO ()) -- ^ Action for setting start-up-time options and logic
  -> ProblemFeatures
  -> Maybe IO.Handle
  -> B.ExprBuilder t st fs
  -> IO (SolverProcess t (Writer a))
startSolver :: a
-> AcknowledgementAction t (Writer a)
-> (WriterConn t (Writer a) -> IO ())
-> ProblemFeatures
-> Maybe Handle
-> ExprBuilder t st fs
-> IO (SolverProcess t (Writer a))
startSolver a
solver AcknowledgementAction t (Writer a)
ack WriterConn t (Writer a) -> IO ()
setup ProblemFeatures
feats Maybe Handle
auxOutput ExprBuilder t st fs
sym = do
  String
path <- a -> ExprBuilder t st fs -> IO String
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a -> ExprBuilder t st fs -> IO String
defaultSolverPath a
solver ExprBuilder t st fs
sym
  [String]
args <- a -> ExprBuilder t st fs -> IO [String]
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs a
solver ExprBuilder t st fs
sym
  hdls :: (Handle, Handle, Handle, ProcessHandle)
hdls@(Handle
in_h, Handle
out_h, Handle
err_h, ProcessHandle
ph) <- String
-> [String]
-> Maybe String
-> IO (Handle, Handle, Handle, ProcessHandle)
startProcess String
path [String]
args Maybe String
forall a. Maybe a
Nothing

  (OutputStream Text
in_stream, InputStream Text
out_stream, HandleReader
err_reader) <-
     Handle
-> Handle
-> Handle
-> Maybe (Text, Handle)
-> IO (OutputStream Text, InputStream Text, HandleReader)
demuxProcessHandles Handle
in_h Handle
out_h Handle
err_h
       ((Handle -> (Text, Handle)) -> Maybe Handle -> Maybe (Text, Handle)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Handle
x -> (Text
"; ", Handle
x)) Maybe Handle
auxOutput)

  -- Create writer
  WriterConn t (Writer a)
writer <- a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> ExprBuilder t st fs
-> OutputStream Text
-> InputStream Text
-> IO (WriterConn t (Writer a))
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> ExprBuilder t st fs
-> OutputStream Text
-> InputStream Text
-> IO (WriterConn t (Writer a))
newDefaultWriter a
solver AcknowledgementAction t (Writer a)
ack ProblemFeatures
feats ExprBuilder t st fs
sym OutputStream Text
in_stream InputStream Text
out_stream

  -- Set solver logic and solver-specific options
  WriterConn t (Writer a) -> IO ()
setup WriterConn t (Writer a)
writer

  -- Query the solver for it's error behavior
  ErrorBehavior
errBeh <- a
-> WriterConn t (Writer a) -> InputStream Text -> IO ErrorBehavior
forall a t.
SMTLib2GenericSolver a =>
a
-> WriterConn t (Writer a) -> InputStream Text -> IO ErrorBehavior
getErrorBehavior a
solver WriterConn t (Writer a)
writer InputStream Text
out_stream

  IORef (Maybe Int)
earlyUnsatRef <- Maybe Int -> IO (IORef (Maybe Int))
forall a. a -> IO (IORef a)
newIORef Maybe Int
forall a. Maybe a
Nothing

  -- push an initial frame for solvers that don't support reset
  Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (a -> Bool
forall a. SMTLib2GenericSolver a => a -> Bool
supportsResetAssertions a
solver) (WriterConn t (Writer a) -> Command (Writer a) -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t (Writer a)
writer (Integer -> Command
SMT2.push Integer
1))

  SolverProcess t (Writer a) -> IO (SolverProcess t (Writer a))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SolverProcess t (Writer a) -> IO (SolverProcess t (Writer a)))
-> SolverProcess t (Writer a) -> IO (SolverProcess t (Writer a))
forall a b. (a -> b) -> a -> b
$! SolverProcess :: forall scope solver.
WriterConn scope solver
-> IO ExitCode
-> ProcessHandle
-> OutputStream Text
-> InputStream Text
-> ErrorBehavior
-> HandleReader
-> SMTEvalFunctions solver
-> (SolverEvent -> IO ())
-> String
-> IORef (Maybe Int)
-> Bool
-> SolverGoalTimeout
-> SolverProcess scope solver
SolverProcess
            { solverConn :: WriterConn t (Writer a)
solverConn     = WriterConn t (Writer a)
writer
            , solverCleanupCallback :: IO ExitCode
solverCleanupCallback = (Handle, Handle, Handle, ProcessHandle) -> IO ExitCode
cleanupProcess (Handle, Handle, Handle, ProcessHandle)
hdls
            , solverStdin :: OutputStream Text
solverStdin    = OutputStream Text
in_stream
            , solverStderr :: HandleReader
solverStderr   = HandleReader
err_reader
            , solverHandle :: ProcessHandle
solverHandle   = ProcessHandle
ph
            , solverErrorBehavior :: ErrorBehavior
solverErrorBehavior = ErrorBehavior
errBeh
            , solverResponse :: InputStream Text
solverResponse = InputStream Text
out_stream
            , solverEvalFuns :: SMTEvalFunctions (Writer a)
solverEvalFuns = WriterConn t (Writer a)
-> InputStream Text -> SMTEvalFunctions (Writer a)
forall h t.
SMTReadWriter h =>
WriterConn t h -> InputStream Text -> SMTEvalFunctions h
smtEvalFuns WriterConn t (Writer a)
writer InputStream Text
out_stream
            , solverLogFn :: SolverEvent -> IO ()
solverLogFn    = ExprBuilder t st fs -> SolverEvent -> IO ()
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
I.logSolverEvent ExprBuilder t st fs
sym
            , solverName :: String
solverName     = a -> String
forall a. Show a => a -> String
show a
solver
            , solverEarlyUnsat :: IORef (Maybe Int)
solverEarlyUnsat = IORef (Maybe Int)
earlyUnsatRef
            , solverSupportsResetAssertions :: Bool
solverSupportsResetAssertions = a -> Bool
forall a. SMTLib2GenericSolver a => a -> Bool
supportsResetAssertions a
solver
            , solverGoalTimeout :: SolverGoalTimeout
solverGoalTimeout = Integer -> SolverGoalTimeout
SolverGoalTimeout Integer
0 -- no timeout by default
            }

shutdownSolver
  :: SMTLib2GenericSolver a => a -> SolverProcess t (Writer a) -> IO (Exit.ExitCode, Lazy.Text)
shutdownSolver :: a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
shutdownSolver a
_solver SolverProcess t (Writer a)
p = do
  -- Tell solver to exit
  WriterConn t (Writer a) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeExit (SolverProcess t (Writer a) -> WriterConn t (Writer a)
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess t (Writer a)
p)
  Text
txt <- HandleReader -> IO Text
readAllLines (SolverProcess t (Writer a) -> HandleReader
forall scope solver. SolverProcess scope solver -> HandleReader
solverStderr SolverProcess t (Writer a)
p)
  HandleReader -> IO ()
stopHandleReader (SolverProcess t (Writer a) -> HandleReader
forall scope solver. SolverProcess scope solver -> HandleReader
solverStderr SolverProcess t (Writer a)
p)
  ExitCode
ec <- SolverProcess t (Writer a) -> IO ExitCode
forall scope solver. SolverProcess scope solver -> IO ExitCode
solverCleanupCallback SolverProcess t (Writer a)
p
  (ExitCode, Text) -> IO (ExitCode, Text)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExitCode
ec,Text
txt)


-----------------------------------------------------------------
-- Checking solver version bounds


-- | Solver version bounds computed from \"solverBounds.config\"
defaultSolverBounds :: Map Text SolverBounds
defaultSolverBounds :: Map Text SolverBounds
defaultSolverBounds = [(Text, SolverBounds)] -> Map Text SolverBounds
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList $(String
[Item [(Text, SolverBounds)]]
[Item [VChunk]]
[Item [VUnit]]
Maybe Word
Word
Item [(Text, SolverBounds)]
Item [VChunk]
String -> Text
Maybe Word -> NonEmpty VChunk -> [VChunk] -> [VChunk] -> Version
Maybe Version -> Maybe Version -> Maybe Version -> SolverBounds
Word -> VUnit
VChunk -> [VChunk] -> NonEmpty VChunk
VUnit -> [VUnit] -> VChunk
Version -> Maybe Version
forall a. Maybe a
forall a. a -> Maybe a
forall a. a -> [a] -> NonEmpty a
computeDefaultSolverBounds)

-- | Things that can go wrong while checking which solver version we've got
data SolverVersionCheckError =
  UnparseableVersion Versions.ParsingError

ppSolverVersionCheckError :: SolverVersionCheckError -> PP.Doc ann
ppSolverVersionCheckError :: SolverVersionCheckError -> Doc ann
ppSolverVersionCheckError SolverVersionCheckError
err =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep
  [ Item [Doc ann]
"Unexpected error while checking solver version:"
  , case SolverVersionCheckError
err of
      UnparseableVersion ParsingError
parseErr ->
        [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.hsep
        [ Item [Doc ann]
"Couldn't parse solver version number:"
        , ParsingError -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow ParsingError
parseErr
        ]
  ]

data SolverVersionError =
  SolverVersionError
  { SolverVersionError -> SolverBounds
vBounds :: SolverBounds
  , SolverVersionError -> Version
vActual :: Version
  }

ppSolverVersionError :: SolverVersionError -> PP.Doc ann
ppSolverVersionError :: SolverVersionError -> Doc ann
ppSolverVersionError SolverVersionError
err =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep
  [ Item [Doc ann]
"Solver did not meet version bound restrictions:"
  , Doc ann
"Lower bound (inclusive):" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Maybe Version -> Doc ann
forall a ann. Show a => Maybe a -> Doc ann
na (SolverBounds -> Maybe Version
lower (SolverVersionError -> SolverBounds
vBounds SolverVersionError
err))
  , Doc ann
"Upper bound (non-inclusive):" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Maybe Version -> Doc ann
forall a ann. Show a => Maybe a -> Doc ann
na (SolverBounds -> Maybe Version
upper (SolverVersionError -> SolverBounds
vBounds SolverVersionError
err))
  , Doc ann
"Actual version:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Version -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow (SolverVersionError -> Version
vActual SolverVersionError
err)
  ]
  where na :: Maybe a -> Doc ann
na (Just a
s) = a -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow a
s
        na Maybe a
Nothing  = Doc ann
"n/a"

-- | Get the result of a version query
nameResult :: SMTReadWriter h => f h -> Streams.InputStream Text -> IO Text
nameResult :: f h -> InputStream Text -> IO Text
nameResult f h
_ InputStream Text
s =
  let cmd :: Command
cmd = Command
SMT2.getName
  in
    (SomeException -> Maybe SomeException)
-> IO SExp -> IO (Either SomeException SExp)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (Parser SExp -> InputStream Text -> IO SExp
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseSMTLib2String) InputStream Text
s) IO (Either SomeException SExp)
-> (Either SomeException SExp -> IO Text) -> IO Text
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>=
      \case
        Right (SApp [SAtom ":name", SString nm]) -> Text -> IO Text
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Text
nm
        Right (SApp [SAtom "error", SString msg]) -> SMTLib2Exception -> IO Text
forall a e. Exception e => e -> a
throw (Command -> Text -> SMTLib2Exception
SMTLib2Error Command
cmd Text
msg)
        Right SExp
res -> SMTLib2Exception -> IO Text
forall a e. Exception e => e -> a
throw ([Command] -> Text -> SMTLib2Exception
SMTLib2ParseError [Item [Command]
Command
cmd] (String -> Text
Text.pack (SExp -> String
forall a. Show a => a -> String
show SExp
res)))
        Left (SomeException e
e) ->
          Text -> Command -> e -> IO Text
forall e (m :: Type -> Type) a.
Exception e =>
Text -> Command -> e -> m a
throwSMTLib2ParseError Text
"name query" Command
cmd e
e


-- | Query the solver's error behavior setting
queryErrorBehavior :: SMTLib2Tweaks a =>
  WriterConn t (Writer a) -> Streams.InputStream Text -> IO ErrorBehavior
queryErrorBehavior :: WriterConn t (Writer a) -> InputStream Text -> IO ErrorBehavior
queryErrorBehavior WriterConn t (Writer a)
conn InputStream Text
resp =
  do let cmd :: Command
cmd = Command
SMT2.getErrorBehavior
     WriterConn t (Writer a) -> Command (Writer a) -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
writeCommand WriterConn t (Writer a)
conn Command
Command (Writer a)
cmd
     (SomeException -> Maybe SomeException)
-> IO SExp -> IO (Either SomeException SExp)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (Parser SExp -> InputStream Text -> IO SExp
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseSMTLib2String) InputStream Text
resp) IO (Either SomeException SExp)
-> (Either SomeException SExp -> IO ErrorBehavior)
-> IO ErrorBehavior
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>=
       \case
         Right (SApp [SAtom ":error-behavior", SAtom "continued-execution"]) -> ErrorBehavior -> IO ErrorBehavior
forall (m :: Type -> Type) a. Monad m => a -> m a
return ErrorBehavior
ContinueOnError
         Right (SApp [SAtom ":error-behavior", SAtom "immediate-exit"]) -> ErrorBehavior -> IO ErrorBehavior
forall (m :: Type -> Type) a. Monad m => a -> m a
return ErrorBehavior
ImmediateExit
         Right SExp
res -> SMTLib2Exception -> IO ErrorBehavior
forall a e. Exception e => e -> a
throw ([Command] -> Text -> SMTLib2Exception
SMTLib2ParseError [Item [Command]
Command
cmd] (String -> Text
Text.pack (SExp -> String
forall a. Show a => a -> String
show SExp
res)))
         Left (SomeException e
e) -> Text -> Command -> e -> IO ErrorBehavior
forall e (m :: Type -> Type) a.
Exception e =>
Text -> Command -> e -> m a
throwSMTLib2ParseError Text
"error behavior query" Command
cmd e
e


-- | Get the result of a version query
versionResult :: SMTReadWriter h => f h -> Streams.InputStream Text -> IO Text
versionResult :: f h -> InputStream Text -> IO Text
versionResult f h
_ InputStream Text
s =
  let cmd :: Command
cmd = Command
SMT2.getVersion
  in
    (SomeException -> Maybe SomeException)
-> IO SExp -> IO (Either SomeException SExp)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (Parser SExp -> InputStream Text -> IO SExp
forall r. Parser r -> InputStream Text -> IO r
Streams.parseFromStream (Parser Text -> Parser SExp
parseSExp Parser Text
parseSMTLib2String) InputStream Text
s) IO (Either SomeException SExp)
-> (Either SomeException SExp -> IO Text) -> IO Text
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>=
      \case
        Right (SApp [SAtom ":version", SString v]) -> Text -> IO Text
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Text
v
        Right (SApp [SAtom "error", SString msg]) -> SMTLib2Exception -> IO Text
forall a e. Exception e => e -> a
throw (Command -> Text -> SMTLib2Exception
SMTLib2Error Command
cmd Text
msg)
        Right SExp
res -> SMTLib2Exception -> IO Text
forall a e. Exception e => e -> a
throw ([Command] -> Text -> SMTLib2Exception
SMTLib2ParseError [Item [Command]
Command
cmd] (String -> Text
Text.pack (SExp -> String
forall a. Show a => a -> String
show SExp
res)))
        Left (SomeException e
e) ->
          Text -> Command -> e -> IO Text
forall e (m :: Type -> Type) a.
Exception e =>
Text -> Command -> e -> m a
throwSMTLib2ParseError Text
"version query" Command
cmd e
e

-- | Ensure the solver's version falls within a known-good range.
checkSolverVersion' :: SMTLib2Tweaks solver =>
  Map Text SolverBounds ->
  SolverProcess scope (Writer solver) ->
  IO (Either SolverVersionCheckError (Maybe SolverVersionError))
checkSolverVersion' :: Map Text SolverBounds
-> SolverProcess scope (Writer solver)
-> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
checkSolverVersion' Map Text SolverBounds
boundsMap SolverProcess scope (Writer solver)
proc =
  let conn :: WriterConn scope (Writer solver)
conn = SolverProcess scope (Writer solver)
-> WriterConn scope (Writer solver)
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope (Writer solver)
proc
      name :: String
name = WriterConn scope (Writer solver) -> String
forall t h. WriterConn t h -> String
smtWriterName WriterConn scope (Writer solver)
conn
      done :: IO (Either a (Maybe a))
done = Either a (Maybe a) -> IO (Either a (Maybe a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe a -> Either a (Maybe a)
forall a b. b -> Either a b
Right Maybe a
forall a. Maybe a
Nothing)
      verr :: SolverBounds -> Version -> f (Either a (Maybe SolverVersionError))
verr SolverBounds
bnds Version
actual = Either a (Maybe SolverVersionError)
-> f (Either a (Maybe SolverVersionError))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe SolverVersionError -> Either a (Maybe SolverVersionError)
forall a b. b -> Either a b
Right (SolverVersionError -> Maybe SolverVersionError
forall a. a -> Maybe a
Just (SolverBounds -> Version -> SolverVersionError
SolverVersionError SolverBounds
bnds Version
actual))) in
  case Text -> Map Text SolverBounds -> Maybe SolverBounds
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (String -> Text
Text.pack String
name) Map Text SolverBounds
boundsMap of
    Maybe SolverBounds
Nothing -> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
forall a a. IO (Either a (Maybe a))
done
    Just SolverBounds
bnds ->
      do WriterConn scope (Writer solver) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
getVersion WriterConn scope (Writer solver)
conn
         Text
res <- WriterConn scope (Writer solver) -> InputStream Text -> IO Text
forall h (f :: Type -> Type).
SMTReadWriter h =>
f h -> InputStream Text -> IO Text
versionResult WriterConn scope (Writer solver)
conn (SolverProcess scope (Writer solver) -> InputStream Text
forall scope solver. SolverProcess scope solver -> InputStream Text
solverResponse SolverProcess scope (Writer solver)
proc)
         case Text -> Either ParsingError Version
Versions.version Text
res of
           Left ParsingError
e -> Either SolverVersionCheckError (Maybe SolverVersionError)
-> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SolverVersionCheckError
-> Either SolverVersionCheckError (Maybe SolverVersionError)
forall a b. a -> Either a b
Left (ParsingError -> SolverVersionCheckError
UnparseableVersion ParsingError
e))
           Right Version
actualVer ->
             case (SolverBounds -> Maybe Version
lower SolverBounds
bnds, SolverBounds -> Maybe Version
upper SolverBounds
bnds) of
               (Maybe Version
Nothing, Maybe Version
Nothing) -> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
forall a a. IO (Either a (Maybe a))
done
               (Maybe Version
Nothing, Just Version
maxVer) ->
                 if Version
actualVer Version -> Version -> Bool
forall a. Ord a => a -> a -> Bool
< Version
maxVer then IO (Either SolverVersionCheckError (Maybe SolverVersionError))
forall a a. IO (Either a (Maybe a))
done else SolverBounds
-> Version
-> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
forall (f :: Type -> Type) a.
Applicative f =>
SolverBounds -> Version -> f (Either a (Maybe SolverVersionError))
verr SolverBounds
bnds Version
actualVer
               (Just Version
minVer, Maybe Version
Nothing) ->
                 if Version
minVer Version -> Version -> Bool
forall a. Ord a => a -> a -> Bool
<= Version
actualVer then IO (Either SolverVersionCheckError (Maybe SolverVersionError))
forall a a. IO (Either a (Maybe a))
done else SolverBounds
-> Version
-> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
forall (f :: Type -> Type) a.
Applicative f =>
SolverBounds -> Version -> f (Either a (Maybe SolverVersionError))
verr SolverBounds
bnds Version
actualVer
               (Just Version
minVer, Just Version
maxVer) ->
                 if Version
minVer Version -> Version -> Bool
forall a. Ord a => a -> a -> Bool
<= Version
actualVer Bool -> Bool -> Bool
&& Version
actualVer Version -> Version -> Bool
forall a. Ord a => a -> a -> Bool
< Version
maxVer then IO (Either SolverVersionCheckError (Maybe SolverVersionError))
forall a a. IO (Either a (Maybe a))
done else SolverBounds
-> Version
-> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
forall (f :: Type -> Type) a.
Applicative f =>
SolverBounds -> Version -> f (Either a (Maybe SolverVersionError))
verr SolverBounds
bnds Version
actualVer


-- | Ensure the solver's version falls within a known-good range.
checkSolverVersion :: SMTLib2Tweaks solver =>
  SolverProcess scope (Writer solver) ->
  IO (Either SolverVersionCheckError (Maybe SolverVersionError))
checkSolverVersion :: SolverProcess scope (Writer solver)
-> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
checkSolverVersion = Map Text SolverBounds
-> SolverProcess scope (Writer solver)
-> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
forall solver scope.
SMTLib2Tweaks solver =>
Map Text SolverBounds
-> SolverProcess scope (Writer solver)
-> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
checkSolverVersion' Map Text SolverBounds
defaultSolverBounds