------------------------------------------------------------------------
-- |
-- 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 FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# 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
  , writeGetAbduct
  , writeGetAbductNext
  , writeCheckSynth
  , runCheckSat
  , runGetAbducts
  , asSMT2Type
  , setOption
  , getVersion
  , versionResult
  , getName
  , nameResult
  , setProduceModels
  , smtLibEvalFuns
  , smtlib2Options
  , parseFnModel
  , parseFnValues
    -- * Logic
  , SMT2.Logic(..)
  , SMT2.qf_bv
  , SMT2.allSupported
  , SMT2.hornLogic
  , all_supported
  , setLogic
    -- * Type
  , SMT2.Sort(..)
  , SMT2.arraySort
    -- * Term
  , Term(..)
  , arrayConst
  , What4.Protocol.SMTLib2.arraySelect
  , arrayStore
    -- * Solvers and External interface
  , Session(..)
  , SMTLib2GenericSolver(..)
  , writeDefaultSMT2
  , defaultFileWriter
  , 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.Except
import           Control.Monad.Reader
import qualified Data.Bimap as Bimap
import qualified Data.BitVector.Sized as BV
import           Data.Char (digitToInt, isAscii)
import           Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as HashMap
import           Data.IORef
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Monoid
import           Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
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 qualified Data.Text as Text
import qualified Data.Text.Lazy as Lazy
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           Data.Versions (Version(..))
import qualified Data.Versions as Versions
import qualified Prettyprinter as PP
import           Text.Printf (printf)
import           LibBF( bfToBits )

import           Prelude hiding (writeFile)

import           What4.BaseTypes
import qualified What4.Config as CFG
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           What4.Protocol.SMTLib2.Response
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.allLogic
{-# DEPRECATED all_supported "Use allLogic instead" #-}


smtlib2Options :: [CFG.ConfigDesc]
smtlib2Options :: [ConfigDesc]
smtlib2Options = [ConfigDesc]
smtParseOptions

------------------------------------------------------------------------
-- 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
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
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
Ord)

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

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

------------------------------------------------------------------------------------
-- String Escaping functions
--
-- The following functions implement the escaping and
-- escape parsing rules from SMTLib 2.6.  Documentation
-- regarding this format is pasted below from the
-- specification document.
--
--      String literals
--      All double-quote-delimited string literals consisting of printable US ASCII
--      characters, i.e., those with Unicode code point from 0x00020 to 0x0007E.
--      We refer to these literals as _string constants_.
--
--      The restriction to printable US ASCII characters in string constants is for
--      simplicity since that set is universally supported. Arbitrary Unicode characters
--      can be represented with _escape sequences_ which can have one of the following
--      forms
--          \ud₃d₂d₁d₀
--          \u{d₀}
--          \u{d₁d₀}
--          \u{d₂d₁d₀}
--          \u{d₃d₂d₁d₀}
--          \u{d₄d₃d₂d₁d₀}
--      where each dᵢ is a hexadecimal digit and d₄ is restricted to the range 0-2.
--      These are the **only escape sequences** in this theory. See later.
--      In a later version, the restrictions above on the digits may be extended
--      to allow characters from all 17 Unicode planes.
--
--      Observe that the first form, \ud₃d₂d₁d₀, has exactly 4 hexadecimal digit,
--      following the common use of this form in some programming languages.
--      Unicode characters outside the range covered by \ud₃d₂d₁d₀ can be
--      represented with the long form \u{d₄d₃d₂d₁d₀}.
--
--      Also observe that programming language-specific escape sequences, such as
--      \n, \b, \r and so on, are _not_ escape sequences in this theory as they
--      are not fully standard across languages.

-- | Apply the SMTLib2.6 string escaping rules to a string literal.
textToTerm :: Text -> Term
textToTerm :: Text -> Term
textToTerm Text
bs = Builder -> Term
SMT2.T (Builder
"\"" forall a. Semigroup a => a -> a -> a
<> forall a. (Char -> a -> a) -> a -> Text -> a
Text.foldr Char -> Builder -> Builder
f Builder
"\"" Text
bs)
 where
 inLiteralRange :: a -> Bool
inLiteralRange a
c = Int
0x20 forall a. Ord a => a -> a -> Bool
<= forall a. Enum a => a -> Int
fromEnum a
c Bool -> Bool -> Bool
&& forall a. Enum a => a -> Int
fromEnum a
c forall a. Ord a => a -> a -> Bool
<= Int
0x7E

 f :: Char -> Builder -> Builder
f Char
c Builder
x
   -- special case: the `"` character has a special case escaping mode which
   -- is encoded as `""`
   | Char
'\"' forall a. Eq a => a -> a -> Bool
== Char
c = Builder
"\"\"" forall a. Semigroup a => a -> a -> a
<> Builder
x

   -- special case: always escape the `\` character as an explicit code point,
   -- so we don't have to do lookahead to discover if it is followed by a `u`
   | Char
'\\' forall a. Eq a => a -> a -> Bool
== Char
c = Builder
"\\u{5c}" forall a. Semigroup a => a -> a -> a
<> Builder
x

   -- others characters in the "normal" ASCII range require no escaping
   | forall {a}. Enum a => a -> Bool
inLiteralRange Char
c = Char -> Builder
Builder.singleton Char
c forall a. Semigroup a => a -> a -> a
<> Builder
x

   -- characters outside that range require escaping
   | Bool
otherwise = Builder
"\\u{" forall a. Semigroup a => a -> a -> a
<> String -> Builder
Builder.fromString (forall a. (Integral a, Show a) => a -> ShowS
showHex (forall a. Enum a => a -> Int
fromEnum Char
c) String
"}") forall a. Semigroup a => a -> a -> a
<> Builder
x



-- | Parse SMTLIb2.6 escaping rules for strings.
--
--   Note! The escaping rule that uses the @\"\"@ sequence
--   to encode a double quote has already been resolved
--   by @parseSMTLIb2String@, so here we just need to
--   parse the @\\u@ escape forms.
unescapeText :: Text -> Maybe Text
unescapeText :: Text -> Maybe Text
unescapeText = Text -> Text -> Maybe Text
go forall a. Monoid a => a
mempty
 where
 go :: Text -> Text -> Maybe Text
go Text
str Text
t =
   case Text -> Maybe (Char, Text)
Text.uncons Text
t of
     Maybe (Char, Text)
Nothing -> forall a. a -> Maybe a
Just Text
str
     Just (Char
c, Text
t')
       | Bool -> Bool
not (Char -> Bool
isAscii Char
c) -> forall a. Maybe a
Nothing
       | Char
c forall a. Eq a => a -> a -> Bool
== Char
'\\'       -> Text -> Text -> Maybe Text
readEscape Text
str Text
t'
       | Bool
otherwise       -> Text -> Char -> Text -> Maybe Text
continue Text
str Char
c Text
t'

 continue :: Text -> Char -> Text -> Maybe Text
continue Text
str Char
c Text
t = Text -> Text -> Maybe Text
go (Text -> Char -> Text
Text.snoc Text
str Char
c) Text
t

 readEscape :: Text -> Text -> Maybe Text
readEscape Text
str Text
t =
   case Text -> Maybe (Char, Text)
Text.uncons Text
t of
     Maybe (Char, Text)
Nothing -> forall a. a -> Maybe a
Just (Text -> Char -> Text
Text.snoc Text
str Char
'\\')
     Just (Char
c, Text
t')
       -- Note: the \u forms are the _only_ escape forms
       | Char
c forall a. Eq a => a -> a -> Bool
== Char
'u'  -> Text -> Text -> Maybe Text
readHexEscape Text
str Text
t'
       | Bool
otherwise -> Text -> Char -> Text -> Maybe Text
continue (Text -> Char -> Text
Text.snoc Text
str Char
'\\') Char
c Text
t'

 readHexEscape :: Text -> Text -> Maybe Text
readHexEscape Text
str Text
t =
   case Text -> Maybe (Char, Text)
Text.uncons Text
t of
     Just (Char
c, Text
t')
       -- take until the closing brace
       | Char
c forall a. Eq a => a -> a -> Bool
== Char
'{'
       , (Text
ds, Text
t'') <- Text -> Text -> (Text, Text)
Text.breakOn Text
"}" Text
t'
       , Just (Char
'}',Text
t''') <- Text -> Maybe (Char, Text)
Text.uncons Text
t''
       -> Text -> Text -> Text -> Maybe Text
readDigits Text
str Text
ds Text
t'''

         -- take exactly four digits
       | (Text
ds, Text
t'') <- Int -> Text -> (Text, Text)
Text.splitAt Int
4 Text
t'
       , Text -> Int
Text.length Text
ds forall a. Eq a => a -> a -> Bool
== Int
4
       -> Text -> Text -> Text -> Maybe Text
readDigits Text
str Text
ds Text
t''

     Maybe (Char, Text)
_ -> forall a. Maybe a
Nothing

 readDigits :: Text -> Text -> Text -> Maybe Text
readDigits Text
str Text
ds Text
t =
    case forall a. (Eq a, Num a) => ReadS a
readHex (Text -> String
Text.unpack Text
ds) of
      (Int
n, []):[(Int, String)]
_ -> Text -> Char -> Text -> Maybe Text
continue Text
str (forall a. Enum a => Int -> a
toEnum Int
n) Text
t
      [(Int, String)]
_ -> 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 = 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 = 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 = forall a. Maybe a
Nothing

  smtlib2arraySelect :: Term -> [Term] -> Term
  smtlib2arraySelect Term
a [] = Term
a
  smtlib2arraySelect Term
a (Term
h:[Term]
l) = 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
      [] -> 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 :: Text -> Term
  smtlib2StringTerm = Text -> Term
textToTerm

  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" [Term
s,Term
t,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" [Term
x,Term
off,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 forall a b. (a -> b) -> a -> b
$ Builder
"(Struct" forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Int
n forall a. Semigroup a => a -> a -> a
<> forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Sort -> Builder
f [Sort]
flds forall a. Semigroup a => a -> a -> a
<> Builder
")"
       where f :: SMT2.Sort -> Builder
             f :: Sort -> Builder
f (SMT2.Sort Builder
s) = Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
s
             n :: Int
n = 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" forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal (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 [Term
a]
    where nm :: Builder
nm = Builder
"struct" forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Int
n forall a. Semigroup a => a -> a -> a
<> Builder
"-proj" forall a. Semigroup a => a -> a -> a
<> 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 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
    Builder -> Command
SMT2.Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-datatype" [ forall a. IsString a => String -> a
fromString String
"Struct0", [Builder] -> Builder
builder_list [ [Builder] -> Builder
builder_list [Builder
"mk-struct0"]]]
  smtlib2declareStructCmd Int
n = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
    let n_str :: Builder
n_str = forall a. IsString a => String -> a
fromString (forall a. Show a => a -> String
show Int
n)
        tp :: Builder
tp = Builder
"Struct" forall a. Semigroup a => a -> a -> a
<> Builder
n_str
        cnstr :: Builder
cnstr = Builder
"mk-struct" forall a. Semigroup a => a -> a -> a
<> Builder
n_str
        idxes :: [Builder]
idxes = forall a b. (a -> b) -> [a] -> [b]
map (forall a. IsString a => String -> a
fromString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) [Int
0 .. Int
nforall a. Num a => a -> a -> a
-Int
1]
        tp_names :: [Builder]
tp_names = [ Builder
"T" forall a. Semigroup a => a -> a -> a
<> Builder
i_str
                   | Builder
i_str <- [Builder]
idxes
                   ]
        flds :: [Builder]
flds = [ Builder -> [Builder] -> Builder
app (Builder
"struct" forall a. Semigroup a => a -> a -> a
<> Builder
n_str forall a. Semigroup a => a -> a -> a
<> Builder
"-proj" forall a. Semigroup a => a -> a -> a
<> Builder
i_str) [ Builder
"T" forall a. Semigroup a => a -> a -> a
<> Builder
i_str ]
               | Builder
i_str <- [Builder]
idxes
               ]
     in Builder -> Command
SMT2.Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-datatype" [ 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 :: forall a (tp :: BaseType). SMTLib2Tweaks a => 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 (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w)
asSMT2Type (FloatTypeMap FloatPrecisionRepr fpp
fpp) = Builder -> Sort
SMT2.Sort forall a b. (a -> b) -> a -> b
$ Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"FloatingPoint" (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)
asSMT2Type TypeMap tp
UnicodeTypeMap = forall a. SMTLib2Tweaks a => Sort
smtlib2StringSort @a
asSMT2Type TypeMap tp
ComplexToStructTypeMap =
  forall a. SMTLib2Tweaks a => [Sort] -> Sort
smtlib2StructSort @a [ Sort
SMT2.realSort, Sort
SMT2.realSort ]
asSMT2Type TypeMap tp
ComplexToArrayTypeMap =
  forall a. SMTLib2Tweaks a => [Sort] -> Sort -> Sort
smtlib2arrayType @a [Sort
SMT2.boolSort] Sort
SMT2.realSort
asSMT2Type (PrimArrayTypeMap Assignment TypeMap (idxl ::> idx)
i TypeMap tp1
r) =
  forall a. SMTLib2Tweaks a => [Sort] -> Sort -> Sort
smtlib2arrayType @a (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
asSMT2Type @a) Assignment TypeMap (idxl ::> idx)
i) (forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap tp1
r)
asSMT2Type (FnArrayTypeMap Assignment TypeMap (idxl ::> idx)
_ TypeMap tp1
_) =
  forall a. HasCallStack => String -> a
error String
"SMTLIB backend does not support function types as first class."
asSMT2Type (StructTypeMap Assignment TypeMap idx
f) =
  forall a. SMTLib2Tweaks a => [Sort] -> Sort
smtlib2StructSort @a (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
asSMT2Type @a) Assignment TypeMap idx
f)

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

------------------------------------------------------------------------
readBin :: Num a => ReadS a
readBin :: forall a. Num a => ReadS a
readBin = forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
readInt a
2 (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 forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => String -> a
fromString (forall a. Show a => a -> String
show RoundingMode
r)

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

newtype Writer a = Writer { forall a. 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 [Term
x, Term
y]
  Term
x - :: Term -> Term -> Term
- Term
y = Term -> [Term] -> Term
SMT2.sub Term
x [Term
y]
  Term
x * :: Term -> Term -> Term
* Term
y = [Term] -> Term
SMT2.mul [Term
x, 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 [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 [Term
x, Integer -> Term
SMT2.numeral Integer
0])
             (Term -> Term -> Term -> Term
SMT2.ite ([Term] -> Term
SMT2.eq [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 :: forall a. SMTLib2Tweaks a => (Text, Some TypeMap) -> (Text, Sort)
varBinding (Text
nm, Some TypeMap x
tp) = (Text
nm, 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 [Term
x,Term
y]
  Term
x ./= :: Term -> Term -> Term
./= Term
y = [Term] -> Term
SMT2.distinct [Term
x,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 = 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)
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 [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 forall v. SupportTermOps v => v -> v -> v
.== forall v. SupportTermOps v => Integer -> v
integerTerm Integer
0
  intDivisible Term
x Natural
k = forall v. SupportTermOps v => v -> v -> v
intMod Term
x (forall v. SupportTermOps v => Integer -> v
integerTerm (forall a. Integral a => a -> Integer
toInteger Natural
k)) forall v. SupportTermOps v => v -> v -> v
.== Term
0

  rationalTerm :: Rational -> Term
rationalTerm Rational
r | Integer
d 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 = forall a. Ratio a -> a
numerator Rational
r
          d :: Integer
d = forall a. Ratio a -> a
denominator Rational
r

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

  bvTerm :: forall (w :: Natural). NatRepr w -> BV w -> Term
bvTerm NatRepr w
w BV w
u = case forall (n :: Natural). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr w
w of
    Left w :~: 0
Refl -> forall a. HasCallStack => String -> a
error String
"Cannot construct BV term with 0 width"
    Right LeqProof 1 w
LeqProof -> forall (w :: Natural). (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 [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 [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 [Term
y]
  bvOr :: Term -> Term -> Term
bvOr  Term
x Term
y = Term -> [Term] -> Term
SMT2.bvor  Term
x [Term
y]
  bvXor :: Term -> Term -> Term
bvXor Term
x Term
y = Term -> [Term] -> Term
SMT2.bvxor Term
x [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 :: forall (w :: Natural).
NatRepr w -> Natural -> Natural -> Term -> Term
bvExtract NatRepr w
_ Natural
b Natural
n Term
x | Natural
n forall a. Ord a => a -> a -> Bool
> Natural
0 = Natural -> Natural -> Term -> Term
SMT2.extract (Natural
bforall a. Num a => a -> a -> a
+Natural
nforall a. Num a => a -> a -> a
-Natural
1) Natural
b Term
x
                    | Bool
otherwise = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"bvExtract given non-positive width " forall a. [a] -> [a] -> [a]
++ 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 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 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 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 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 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) [Term
x, Term
y, Term
z]

  floatEq :: Term -> Term -> Term
floatEq Term
x Term
y  = [Term] -> Term
SMT2.eq [Term
x,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 :: forall (fpp :: FloatPrecision).
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" (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)) (forall v (w :: Natural). SupportTermOps v => NatRepr w -> BV w -> v
bvTerm NatRepr (eb + sb)
w BV (eb + sb)
bv)
    where
      w :: NatRepr (eb + sb)
w = forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr eb
eb NatRepr sb
sb
      bv :: BV (eb + sb)
bv = forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr (eb + sb)
w (BFOpts -> BigFloat -> Integer
bfToBits (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
fppOpts FloatPrecisionRepr fpp
fpp RoundingMode
RNE) BigFloat
bf)

  floatCast :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term
floatCast FloatPrecisionRepr fpp
fpp RoundingMode
r = Builder -> Term -> Term
un_app forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp (Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"to_fp" (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)) RoundingMode
r
  floatRound :: RoundingMode -> Term -> Term
floatRound RoundingMode
r = Builder -> Term -> Term
un_app forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp Builder
"fp.roundToIntegral" RoundingMode
r
  floatFromBinary :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> Term -> Term
floatFromBinary FloatPrecisionRepr fpp
fpp = Builder -> Term -> Term
un_app forall a b. (a -> b) -> a -> b
$ Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"to_fp" (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)
  bvToFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term
bvToFloat FloatPrecisionRepr fpp
fpp RoundingMode
r =
    Builder -> Term -> Term
un_app forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp (Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"to_fp_unsigned" (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)) RoundingMode
r
  sbvToFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term
sbvToFloat FloatPrecisionRepr fpp
fpp RoundingMode
r = Builder -> Term -> Term
un_app forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp (Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"to_fp" (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> SMTFloatPrecision
asSMTFloatPrecision FloatPrecisionRepr fpp
fpp)) RoundingMode
r
  realToFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term
realToFloat FloatPrecisionRepr fpp
fpp RoundingMode
r = Builder -> Term -> Term
un_app forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp (Builder -> SMTFloatPrecision -> Builder
mkFloatSymbol Builder
"to_fp" (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 forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp (Builder
"(_ fp.to_ubv " forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => String -> a
fromString (forall a. Show a => a -> String
show Natural
w) 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 forall a b. (a -> b) -> a -> b
$ Builder -> RoundingMode -> Builder
mkRoundingOp (Builder
"(_ fp.to_sbv " forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => String -> a
fromString (forall a. Show a => a -> String
show Natural
w) 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../ [Term
y]
  realSin :: Term -> Term
realSin = Builder -> Term -> Term
un_app Builder
"sin"
  realCos :: Term -> Term
realCos = Builder -> Term -> Term
un_app Builder
"cos"
  realTan :: Term -> Term
realTan = Builder -> Term -> Term
un_app Builder
"tan"
  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"
  realTanh :: Term -> Term
realTanh = Builder -> Term -> Term
un_app Builder
"tanh"
  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
          -> ResponseStrictness
             -- ^ Be strict in parsing SMT solver responses?
          -> 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 :: forall a t.
a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> ResponseStrictness
-> 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 ResponseStrictness
isStrict String
solver_name Bool
permitDefineFun ProblemFeatures
arithOption Bool
quantSupport SymbolVarBimap t
bindings = do
  IORef (Set Int)
r <- forall a. a -> IO (IORef a)
newIORef forall a. Set a
Set.empty
  let initWriter :: Writer a
initWriter =
        Writer
        { declaredTuples :: IORef (Set Int)
declaredTuples = IORef (Set Int)
r
        }
  WriterConn t (Writer a)
conn <- forall t cs.
OutputStream Text
-> InputStream Text
-> AcknowledgementAction t cs
-> String
-> ResponseStrictness
-> ProblemFeatures
-> SymbolVarBimap t
-> cs
-> IO (WriterConn t cs)
newWriterConn OutputStream Text
h InputStream Text
in_h AcknowledgementAction t (Writer a)
ack String
solver_name ResponseStrictness
isStrict ProblemFeatures
arithOption SymbolVarBimap t
bindings Writer a
initWriter
  forall (m :: Type -> Type) a. Monad m => a -> m a
return 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_ (forall a. SMTLib2Tweaks a => (Text, Some TypeMap) -> (Text, Sort)
varBinding @a forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
vars) 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_ (forall a. SMTLib2Tweaks a => (Text, Some TypeMap) -> (Text, Sort)
varBinding @a forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
vars) Term (Writer a)
t

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

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

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

  assertNamedCommand :: forall (f :: Type -> Type).
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 (Writer a)
e Text
nm

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

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

  getUnsatAssumptionsCommand :: forall (f :: Type -> Type). f (Writer a) -> Command (Writer a)
getUnsatAssumptionsCommand f (Writer a)
_ = Command
SMT2.getUnsatAssumptions
  getUnsatCoreCommand :: forall (f :: Type -> Type). f (Writer a) -> Command (Writer a)
getUnsatCoreCommand f (Writer a)
_ = Command
SMT2.getUnsatCore
  getAbductCommand :: forall (f :: Type -> Type).
f (Writer a) -> Text -> Term (Writer a) -> Command (Writer a)
getAbductCommand f (Writer a)
_ Text
nm Term (Writer a)
e = Text -> Term -> Command
SMT2.getAbduct Text
nm Term (Writer a)
e
  getAbductNextCommand :: forall (f :: Type -> Type). f (Writer a) -> Command (Writer a)
getAbductNextCommand f (Writer a)
_ = Command
SMT2.getAbductNext
  
  setOptCommand :: forall (f :: Type -> Type).
f (Writer a) -> Text -> Text -> Command (Writer a)
setOptCommand f (Writer a)
_ = Text -> Text -> Command
SMT2.setOption

  declareCommand :: forall (f :: Type -> Type) (args :: Ctx BaseType)
       (rtp :: BaseType).
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 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
asSMT2Type @a) Assignment TypeMap args
argTypes) (forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap rtp
retType)

  defineCommand :: forall (f :: Type -> Type) (rtp :: BaseType).
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, 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 forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Some TypeMap)]
args) (forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap rtp
return_type) Term (Writer a)
e

  synthFunCommand :: forall (f :: Type -> Type) (tp :: BaseType).
f (Writer a)
-> Text
-> [(Text, Some TypeMap)]
-> TypeMap tp
-> Command (Writer a)
synthFunCommand f (Writer a)
_proxy Text
f [(Text, Some TypeMap)]
args TypeMap tp
ret_tp =
    Text -> [(Text, Sort)] -> Sort -> Command
SMT2.synthFun Text
f (forall a b. (a -> b) -> [a] -> [b]
map (\(Text
var, Some TypeMap x
tp) -> (Text
var, forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap x
tp)) [(Text, Some TypeMap)]
args) (forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap tp
ret_tp)
  declareVarCommand :: forall (f :: Type -> Type) (tp :: BaseType).
f (Writer a) -> Text -> TypeMap tp -> Command (Writer a)
declareVarCommand f (Writer a)
_proxy Text
v TypeMap tp
tp = Text -> Sort -> Command
SMT2.declareVar Text
v (forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort
asSMT2Type @a TypeMap tp
tp)
  constraintCommand :: forall (f :: Type -> Type).
f (Writer a) -> Term (Writer a) -> Command (Writer a)
constraintCommand f (Writer a)
_proxy Term (Writer a)
e = Term -> Command
SMT2.constraint Term (Writer a)
e

  stringTerm :: Text -> Term (Writer a)
stringTerm Text
str = forall a. SMTLib2Tweaks a => Text -> Term
smtlib2StringTerm @a Text
str
  stringLength :: Term (Writer a) -> Term (Writer a)
stringLength Term (Writer a)
x = forall a. SMTLib2Tweaks a => Term -> Term
smtlib2StringLength @a Term (Writer a)
x
  stringAppend :: [Term (Writer a)] -> Term (Writer a)
stringAppend [Term (Writer a)]
xs = forall a. SMTLib2Tweaks a => [Term] -> Term
smtlib2StringAppend @a [Term (Writer a)]
xs
  stringContains :: Term (Writer a) -> Term (Writer a) -> Term (Writer a)
stringContains Term (Writer a)
x Term (Writer a)
y = forall a. SMTLib2Tweaks a => Term -> Term -> Term
smtlib2StringContains @a Term (Writer a)
x Term (Writer a)
y
  stringIsPrefixOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a)
stringIsPrefixOf Term (Writer a)
x Term (Writer a)
y = forall a. SMTLib2Tweaks a => Term -> Term -> Term
smtlib2StringIsPrefixOf @a Term (Writer a)
x Term (Writer a)
y
  stringIsSuffixOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a)
stringIsSuffixOf Term (Writer a)
x Term (Writer a)
y = forall a. SMTLib2Tweaks a => Term -> Term -> Term
smtlib2StringIsSuffixOf @a Term (Writer a)
x 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 = forall a. SMTLib2Tweaks a => Term -> Term -> Term -> Term
smtlib2StringIndexOf @a Term (Writer a)
x Term (Writer a)
y 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 = forall a. SMTLib2Tweaks a => Term -> Term -> Term -> Term
smtlib2StringSubstring @a Term (Writer a)
x Term (Writer a)
off Term (Writer a)
len

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

  structProj :: forall (args :: Ctx BaseType) (tp :: BaseType).
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 = forall {k} (ctx :: Ctx k). Size ctx -> Int
Ctx.sizeInt (forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment TypeMap args
tps)
        i :: Int
i = forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal Index args tp
idx
     in forall a. SMTLib2Tweaks a => Int -> Int -> Term -> Term
smtlib2StructProj @a Int
n Int
i Term (Writer a)
v

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

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

  writeCommand :: forall t. WriterConn t (Writer a) -> Command (Writer a) -> IO ()
writeCommand WriterConn t (Writer a)
conn (SMT2.Cmd Builder
cmd) =
    do let cmdout :: Text
cmdout = Text -> Text
Lazy.toStrict (Builder -> Text
Builder.toLazyText Builder
cmd)
       forall a. Maybe a -> OutputStream a -> IO ()
Streams.write (forall a. a -> Maybe a
Just (Text
cmdout forall a. Semigroup a => a -> a -> a
<> Text
"\n")) (forall t h. WriterConn t h -> OutputStream Text
connHandle WriterConn t (Writer a)
conn)
       -- force a flush
       forall a. Maybe a -> OutputStream a -> IO ()
Streams.write (forall a. a -> Maybe a
Just 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 :: forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeCheckSat WriterConn t (Writer a)
w = forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t (Writer a)
w Command
SMT2.checkSat

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

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

setOption :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Text -> Text -> IO ()
setOption :: forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
setOption WriterConn t (Writer a)
w Text
nm Text
val = forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t (Writer a)
w 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 :: forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
getVersion WriterConn t (Writer a)
w = forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
writeCommand WriterConn t (Writer a)
w forall a b. (a -> b) -> a -> b
$ Command
SMT2.getVersion

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

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

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

writeGetAbduct :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Text -> Term -> IO ()
writeGetAbduct :: forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Term -> IO ()
writeGetAbduct WriterConn t (Writer a)
w Text
nm Term
p = forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t (Writer a)
w forall a b. (a -> b) -> a -> b
$ Text -> Term -> Command
SMT2.getAbduct Text
nm Term
p

writeGetAbductNext :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeGetAbductNext :: forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeGetAbductNext WriterConn t (Writer a)
w = forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn t (Writer a)
w Command
SMT2.getAbductNext

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

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

parseIntSolverValue :: MonadFail m => SExp -> m Integer
parseIntSolverValue :: forall (m :: Type -> Type). MonadFail m => SExp -> m Integer
parseIntSolverValue = \case
  SAtom Text
v
    | [(Integer
i, String
"")] <- forall a. (Eq a, Num a) => ReadS a
readDec (Text -> String
Text.unpack Text
v) ->
      forall (m :: Type -> Type) a. Monad m => a -> m a
return Integer
i
  SApp [Item [SExp]
"-", Item [SExp]
x] ->
    forall a. Num a => a -> a
negate forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type). MonadFail m => SExp -> m Integer
parseIntSolverValue Item [SExp]
x
  SExp
s ->
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Could not parse solver value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExp
s

parseRealSolverValue :: MonadFail m => SExp -> m Rational
parseRealSolverValue :: forall (m :: Type -> Type). MonadFail m => SExp -> m Rational
parseRealSolverValue (SAtom Text
v) | Just (Rational
r,String
"") <- forall (m :: Type -> Type).
MonadFail m =>
String -> m (Rational, String)
readDecimal (Text -> String
Text.unpack Text
v) =
  forall (m :: Type -> Type) a. Monad m => a -> m a
return Rational
r
parseRealSolverValue (SApp [Item [SExp]
"-", Item [SExp]
x]) = do
  forall a. Num a => a -> a
negate forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type). MonadFail m => SExp -> m Rational
parseRealSolverValue Item [SExp]
x
parseRealSolverValue (SApp [Item [SExp]
"/", Item [SExp]
x , Item [SExp]
y]) = do
  forall a. Fractional a => a -> a -> a
(/) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type). MonadFail m => SExp -> m Rational
parseRealSolverValue Item [SExp]
x
      forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (m :: Type -> Type). MonadFail m => SExp -> m Rational
parseRealSolverValue Item [SExp]
y
parseRealSolverValue SExp
s = forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Could not parse solver value: " forall a. [a] -> [a] -> [a]
++ 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 :: forall (m :: Type -> Type) (w :: Natural).
MonadFail m =>
NatRepr w -> SExp -> m (BV w)
parseBvSolverValue NatRepr w
w SExp
s
  | Just (Pair NatRepr tp
w' BV tp
bv) <- SExp -> Maybe (Pair NatRepr BV)
parseBVLitHelper SExp
s = case NatRepr tp
w' forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatComparison m n
`compareNat` NatRepr w
w of
      NatLT NatRepr y
zw -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (w :: Natural) (w' :: Natural).
((w + 1) <= w') =>
NatRepr w' -> BV w -> BV w'
BV.zext (forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr tp
w' (forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr y
zw forall (n :: Natural). KnownNat n => NatRepr n
knownNat)) BV tp
bv)
      NatComparison tp w
NatEQ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return BV tp
bv
      NatGT NatRepr y
_ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (w' :: Natural) (w :: Natural).
((w' + 1) <= w) =>
NatRepr w' -> BV w -> BV w'
BV.trunc NatRepr w
w BV tp
bv)
  | Bool
otherwise = forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Could not parse bitvector solver value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExp
s

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 -> forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair NatRepr x
w (forall (w :: Natural). 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 -> Maybe (Pair NatRepr BV.BV)
parseBVLitHelper :: SExp -> Maybe (Pair NatRepr BV)
parseBVLitHelper (SAtom (Text -> String
Text.unpack -> (Char
'#' : Char
'b' : String
n_str))) | [(Integer
n, String
"")] <- forall a. Num a => ReadS a
readBin String
n_str =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Natural -> Integer -> Pair NatRepr BV
natBV (forall a b. (Integral a, Num b) => a -> b
fromIntegral (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))) | [(Integer
n, String
"")] <- forall a. (Eq a, Num a) => ReadS a
readHex String
n_str =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Natural -> Integer -> Pair NatRepr BV
natBV (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (t :: Type -> Type) a. Foldable t => t a -> Int
length String
n_str forall a. Num a => a -> a -> a
* Int
4)) Integer
n
parseBVLitHelper (SApp [Item [SExp]
"_", SAtom (Text -> String
Text.unpack -> (Char
'b' : Char
'v' : String
n_str)), SAtom (Text -> String
Text.unpack -> String
w_str)])
  | [(Integer
n, String
"")] <- forall a. (Eq a, Num a) => ReadS a
readDec String
n_str, [(Natural
w, String
"")] <- forall a. (Eq a, Num a) => ReadS a
readDec String
w_str = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Natural -> Integer -> Pair NatRepr BV
natBV Natural
w Integer
n
parseBVLitHelper SExp
_ = forall a. Maybe a
Nothing

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

parseFloatSolverValue :: MonadFail m => FloatPrecisionRepr fpp
                      -> SExp
                      -> m (BV.BV (FloatPrecisionBits fpp))
parseFloatSolverValue :: forall (m :: Type -> Type) (fpp :: FloatPrecision).
MonadFail m =>
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 <- forall (m :: Type -> Type).
MonadFail m =>
SExp -> m ParsedFloatResult
parseFloatLitHelper SExp
s
  case (NatRepr 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 forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` ((forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) forall (m :: Natural) (n :: Natural).
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 <- forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> (m + n) :~: (n + m)
plusComm NatRepr eb
eb' (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1)
      -- (eb' + 1) + sb' ~ eb' + (1 + sb')
      (eb + sb) :~: ((eb + 1) + sb)
Refl <- forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural) (h :: Natural -> Type) (o :: Natural).
f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o)
plusAssoc NatRepr eb
eb' (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) NatRepr sb
sb'
      forall (m :: Type -> Type) a. Monad m => a -> m a
return BV ((1 + eb) + sb)
bv
        where bv :: BV ((1 + eb) + sb)
bv = forall (w :: Natural) (w' :: Natural).
NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
BV.concat (forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) NatRepr eb
eb) NatRepr sb
sb' (forall (w :: Natural) (w' :: Natural).
NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
BV.concat forall (n :: Natural). KnownNat n => NatRepr n
knownNat NatRepr eb
eb BV 1
sgn BV eb
expt) BV sb
sig
    (Maybe (eb :~: eb), Maybe (sb :~: (1 + sb)))
_ -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Unexpected float precision: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show NatRepr eb
eb' forall a. Semigroup a => a -> a -> a
<> String
", " forall a. Semigroup a => a -> a -> a
<> 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 :: forall (m :: Type -> Type).
MonadFail m =>
SExp -> m ParsedFloatResult
parseFloatLitHelper (SApp [Item [SExp]
"fp", Item [SExp]
sign_s, Item [SExp]
expt_s, Item [SExp]
scand_s])
  | Just (Pair NatRepr tp
sign_w BV tp
sign) <- SExp -> Maybe (Pair NatRepr BV)
parseBVLitHelper Item [SExp]
sign_s
  , Just tp :~: 1
Refl <- NatRepr tp
sign_w forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1)
  , Just (Pair NatRepr tp
eb BV tp
expt) <- SExp -> Maybe (Pair NatRepr BV)
parseBVLitHelper Item [SExp]
expt_s
  , Just (Pair NatRepr tp
sb BV tp
scand) <- SExp -> Maybe (Pair NatRepr BV)
parseBVLitHelper Item [SExp]
scand_s
  = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (eb :: Natural) (sb :: Natural).
BV 1
-> NatRepr eb -> BV eb -> NatRepr sb -> BV sb -> ParsedFloatResult
ParsedFloatResult BV tp
sign NatRepr tp
eb BV tp
expt NatRepr tp
sb BV tp
scand
parseFloatLitHelper
  s :: SExp
s@(SApp [Item [SExp]
"_", SAtom (Text -> String
Text.unpack -> String
nm), SAtom (Text -> String
Text.unpack -> String
eb_s), SAtom (Text -> String
Text.unpack -> String
sb_s)])
  | [(Natural
eb_n, String
"")] <- forall a. (Eq a, Num a) => ReadS a
readDec String
eb_s, [(Natural
sb_n, String
"")] <- 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_nforall a. Num a => a -> a -> a
-Natural
1)
  = case String
nm of
      String
"+oo"   -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (eb :: Natural) (sb :: Natural).
BV 1
-> NatRepr eb -> BV eb -> NatRepr sb -> BV sb -> ParsedFloatResult
ParsedFloatResult (forall (w :: Natural). NatRepr w -> BV w
BV.zero forall (n :: Natural). KnownNat n => NatRepr n
knownNat) NatRepr x
eb (forall (w :: Natural). NatRepr w -> BV w
BV.maxUnsigned NatRepr x
eb) NatRepr x
sb (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr x
sb)
      String
"-oo"   -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (eb :: Natural) (sb :: Natural).
BV 1
-> NatRepr eb -> BV eb -> NatRepr sb -> BV sb -> ParsedFloatResult
ParsedFloatResult (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.one forall (n :: Natural). KnownNat n => NatRepr n
knownNat)  NatRepr x
eb (forall (w :: Natural). NatRepr w -> BV w
BV.maxUnsigned NatRepr x
eb) NatRepr x
sb (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr x
sb)
      String
"+zero" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (eb :: Natural) (sb :: Natural).
BV 1
-> NatRepr eb -> BV eb -> NatRepr sb -> BV sb -> ParsedFloatResult
ParsedFloatResult (forall (w :: Natural). NatRepr w -> BV w
BV.zero forall (n :: Natural). KnownNat n => NatRepr n
knownNat) NatRepr x
eb (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr x
eb)        NatRepr x
sb (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr x
sb)
      String
"-zero" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (eb :: Natural) (sb :: Natural).
BV 1
-> NatRepr eb -> BV eb -> NatRepr sb -> BV sb -> ParsedFloatResult
ParsedFloatResult (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.one forall (n :: Natural). KnownNat n => NatRepr n
knownNat)  NatRepr x
eb (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr x
eb)        NatRepr x
sb (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr x
sb)
      String
"NaN"   -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (eb :: Natural) (sb :: Natural).
BV 1
-> NatRepr eb -> BV eb -> NatRepr sb -> BV sb -> ParsedFloatResult
ParsedFloatResult (forall (w :: Natural). NatRepr w -> BV w
BV.zero forall (n :: Natural). KnownNat n => NatRepr n
knownNat) NatRepr x
eb (forall (w :: Natural). NatRepr w -> BV w
BV.maxUnsigned NatRepr x
eb) NatRepr x
sb (forall (w :: Natural). NatRepr w -> BV w
BV.maxUnsigned NatRepr x
sb)
      String
_       -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Could not parse float solver value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExp
s
parseFloatLitHelper SExp
s = forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Could not parse float solver value: " forall a. [a] -> [a] -> [a]
++ 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 :: forall (m :: Type -> Type) (w :: Natural) (v :: Natural).
(MonadFail m, 1 <= w, 1 <= v) =>
NatRepr w
-> NatRepr v
-> SExp
-> m (Maybe
        (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
parseBvArraySolverValue NatRepr w
_ NatRepr v
v (SApp [SApp [Item [SExp]
"as", Item [SExp]
"const", Item [SExp]
_], Item [SExp]
c]) = do
  BV v
c' <- forall (m :: Type -> Type) (w :: Natural).
MonadFail m =>
NatRepr w -> SExp -> m (BV w)
parseBvSolverValue NatRepr v
v Item [SExp]
c
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete BV v
c' 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' <- forall (m :: Type -> Type) (w :: Natural) (v :: Natural).
(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]
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' <- forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> IndexLit ('BaseBVType w)
B.BVIndexLit NatRepr w
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type) (w :: Natural).
MonadFail m =>
NatRepr w -> SExp -> m (BV w)
parseBvSolverValue NatRepr w
w Item [SExp]
idx
      BV v
val' <- forall (m :: Type -> Type) (w :: Natural).
MonadFail m =>
NatRepr w -> SExp -> m (BV w)
parseBvSolverValue NatRepr v
v Item [SExp]
val
      forall (m :: Type -> Type) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (idx :: Ctx BaseType) (b :: BaseType).
GroundValue b
-> Map (Assignment IndexLit idx) (GroundValue b)
-> GroundArray idx b
ArrayConcrete GroundValue (BaseBVType v)
base (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty 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)))
  (GroundValue (BaseBVType v))
m)
    Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))
_ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
parseBvArraySolverValue NatRepr w
_ NatRepr v
_ SExp
_ = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

parseFnModel ::
  sym ~ B.ExprBuilder t st fs  =>
  sym ->
  WriterConn t h ->
  [I.SomeSymFn sym] ->
  SExp ->
  IO (MapF (I.SymFnWrapper sym) (I.SymFnWrapper sym))
parseFnModel :: forall sym t (st :: Type -> Type) fs h.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t h
-> [SomeSymFn sym]
-> SExp
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
parseFnModel = forall sym t (st :: Type -> Type) fs h.
(sym ~ ExprBuilder t st fs) =>
(sym -> SExp -> IO (Text, SomeSymFn sym))
-> sym
-> WriterConn t h
-> [SomeSymFn sym]
-> SExp
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
parseFns forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> IO (Text, SomeSymFn sym)
parseDefineFun

parseFnValues ::
  sym ~ B.ExprBuilder t st fs  =>
  sym ->
  WriterConn t h ->
  [I.SomeSymFn sym] ->
  SExp ->
  IO (MapF (I.SymFnWrapper sym) (I.SymFnWrapper sym))
parseFnValues :: forall sym t (st :: Type -> Type) fs h.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t h
-> [SomeSymFn sym]
-> SExp
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
parseFnValues = forall sym t (st :: Type -> Type) fs h.
(sym ~ ExprBuilder t st fs) =>
(sym -> SExp -> IO (Text, SomeSymFn sym))
-> sym
-> WriterConn t h
-> [SomeSymFn sym]
-> SExp
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
parseFns forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> IO (Text, SomeSymFn sym)
parseLambda

parseFns ::
  sym ~ B.ExprBuilder t st fs =>
  (sym -> SExp -> IO (Text, I.SomeSymFn sym)) ->
  sym ->
  WriterConn t h ->
  [I.SomeSymFn sym] ->
  SExp ->
  IO (MapF (I.SymFnWrapper sym) (I.SymFnWrapper sym))
parseFns :: forall sym t (st :: Type -> Type) fs h.
(sym ~ ExprBuilder t st fs) =>
(sym -> SExp -> IO (Text, SomeSymFn sym))
-> sym
-> WriterConn t h
-> [SomeSymFn sym]
-> SExp
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
parseFns sym -> SExp -> IO (Text, SomeSymFn sym)
parse_model_fn sym
sym WriterConn t h
conn [SomeSymFn sym]
uninterp_fns SExp
sexp = do
  Bimap (SomeExprSymFn t) Text
fn_name_bimap <- forall t h.
WriterConn t h
-> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text)
cacheLookupFnNameBimap WriterConn t h
conn forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(I.SomeSymFn SymFn sym args ret
fn) -> forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SomeExprSymFn t
B.SomeExprSymFn SymFn sym args ret
fn) [SomeSymFn sym]
uninterp_fns
  Map Text (SomeSymFn sym)
defined_fns <- case SExp
sexp of
    SApp [SExp]
sexps -> forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (sym -> SExp -> IO (Text, SomeSymFn sym)
parse_model_fn sym
sym) [SExp]
sexps
    SExp
_ -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Could not parse model response: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExp
sexp
  forall {v} (k :: v -> Type) (a :: v -> Type).
OrdF k =>
[Pair k a] -> MapF k a
MapF.fromList forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM
    (\(I.SomeSymFn SymFn sym args ret
uninterp_fn) -> if
      | Just Text
nm <- forall a b (m :: Type -> Type).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
Bimap.lookup (forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SomeExprSymFn t
B.SomeExprSymFn SymFn sym args ret
uninterp_fn) Bimap (SomeExprSymFn t) Text
fn_name_bimap
      , Just (I.SomeSymFn SymFn sym args ret
defined_fn) <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
nm Map Text (SomeSymFn sym)
defined_fns
      , Just args :~: args
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> Assignment BaseTypeRepr args
I.fnArgTypes SymFn sym args ret
uninterp_fn) (forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> Assignment BaseTypeRepr args
I.fnArgTypes SymFn sym args ret
defined_fn)
      , Just ret :~: ret
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
I.fnReturnType SymFn sym args ret
uninterp_fn) (forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
I.fnReturnType SymFn sym args ret
defined_fn) ->
        forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
MapF.Pair (forall sym (args :: Ctx BaseType) (ret :: BaseType).
SymFn sym args ret -> SymFnWrapper sym (args '::> ret)
I.SymFnWrapper SymFn sym args ret
uninterp_fn) (forall sym (args :: Ctx BaseType) (ret :: BaseType).
SymFn sym args ret -> SymFnWrapper sym (args '::> ret)
I.SymFnWrapper SymFn sym args ret
defined_fn)
      | Bool
otherwise -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Could not find model for function: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SymFn sym args ret
uninterp_fn)
    [SomeSymFn sym]
uninterp_fns

parseDefineFun :: I.IsSymExprBuilder sym => sym -> SExp -> IO (Text, I.SomeSymFn sym)
parseDefineFun :: forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> IO (Text, SomeSymFn sym)
parseDefineFun sym
sym SExp
sexp = case SExp
sexp of
  SApp [Item [SExp]
"define-fun", SAtom Text
nm, SApp [SExp]
params_sexp, Item [SExp]
_ret_type_sexp , Item [SExp]
body_sexp] -> do
    SomeSymFn sym
fn <- forall sym.
IsSymExprBuilder sym =>
sym -> Text -> [SExp] -> SExp -> IO (SomeSymFn sym)
parseFn sym
sym Text
nm [SExp]
params_sexp Item [SExp]
body_sexp
    forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text
nm, SomeSymFn sym
fn)
  SExp
_ -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"unexpected sexp, expected define-fun, found " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExp
sexp

parseLambda :: I.IsSymExprBuilder sym => sym -> SExp -> IO (Text, I.SomeSymFn sym)
parseLambda :: forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> IO (Text, SomeSymFn sym)
parseLambda sym
sym SExp
sexp = case SExp
sexp of
  SApp [SAtom Text
nm, SApp [Item [SExp]
"lambda", SApp [SExp]
params_sexp, Item [SExp]
body_sexp]] -> do
    SomeSymFn sym
fn <- forall sym.
IsSymExprBuilder sym =>
sym -> Text -> [SExp] -> SExp -> IO (SomeSymFn sym)
parseFn sym
sym Text
nm [SExp]
params_sexp Item [SExp]
body_sexp
    forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text
nm, SomeSymFn sym
fn)
  SExp
_ -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"unexpected sexp, expected lambda, found " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExp
sexp

parseFn :: I.IsSymExprBuilder sym => sym -> Text -> [SExp] -> SExp -> IO (I.SomeSymFn sym)
parseFn :: forall sym.
IsSymExprBuilder sym =>
sym -> Text -> [SExp] -> SExp -> IO (SomeSymFn sym)
parseFn sym
sym Text
nm [SExp]
params_sexp SExp
body_sexp = do
  ([Text]
nms, [Some (BoundVar sym)]
vars) <- forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> IO (Text, Some (BoundVar sym))
parseVar sym
sym) [SExp]
params_sexp
  case forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList [Some (BoundVar sym)]
vars of
    Some Assignment (BoundVar sym) x
vars_assign -> do
      let let_env :: HashMap Text (Some (SymExpr sym))
let_env = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
nms forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall {k} (f :: k -> Type) (g :: k -> Type).
(forall (tp :: k). f tp -> g tp) -> Some f -> Some g
mapSome forall a b. (a -> b) -> a -> b
$ forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> SymExpr sym tp
I.varExpr sym
sym) [Some (BoundVar sym)]
vars
      Either String (Some (SymExpr sym))
proc_res <- forall sym a.
ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor (ProcessorEnv { procSym :: sym
procSym = sym
sym, procLetEnv :: HashMap Text (Some (SymExpr sym))
procLetEnv = HashMap Text (Some (SymExpr sym))
let_env }) forall a b. (a -> b) -> a -> b
$ forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym SExp
body_sexp
      Some SymExpr sym x
body_expr <- forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall (m :: Type -> Type) a. Monad m => a -> m a
return Either String (Some (SymExpr sym))
proc_res
      forall sym (args :: Ctx BaseType) (ret :: BaseType).
SymFn sym args ret -> SomeSymFn sym
I.SomeSymFn forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment (BoundVar sym) args
-> SymExpr sym ret
-> UnfoldPolicy
-> IO (SymFn sym args ret)
I.definedFn sym
sym (String -> SolverSymbol
I.safeSymbol forall a b. (a -> b) -> a -> b
$ Text -> String
Text.unpack Text
nm) Assignment (BoundVar sym) x
vars_assign SymExpr sym x
body_expr UnfoldPolicy
I.NeverUnfold

parseVar :: I.IsSymExprBuilder sym => sym -> SExp -> IO (Text, Some (I.BoundVar sym))
parseVar :: forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> IO (Text, Some (BoundVar sym))
parseVar sym
sym SExp
sexp = case SExp
sexp of
  SApp [SAtom Text
nm, Item [SExp]
tp_sexp] -> do
    Some BaseTypeRepr x
tp <- SExp -> IO (Some BaseTypeRepr)
parseType Item [SExp]
tp_sexp
    BoundVar sym x
var <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
I.freshBoundVar sym
sym (String -> SolverSymbol
I.safeSymbol forall a b. (a -> b) -> a -> b
$ Text -> String
Text.unpack Text
nm) BaseTypeRepr x
tp
    forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text
nm, forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BoundVar sym x
var)
  SExp
_ -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"unexpected variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExp
sexp

parseType :: SExp -> IO (Some BaseTypeRepr)
parseType :: SExp -> IO (Some BaseTypeRepr)
parseType SExp
sexp = case SExp
sexp of
  SExp
"Bool" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseBoolType
BaseBoolRepr
  SExp
"Int" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseIntegerType
BaseIntegerRepr
  SExp
"Real" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseRealType
BaseRealRepr
  SApp [Item [SExp]
"_", Item [SExp]
"BitVec", SAtom (Text -> String
Text.unpack -> String
m_str)]
    | [(Natural
m_n, String
"")] <- forall a. (Eq a, Num a) => ReadS a
readDec String
m_str
    , Some NatRepr x
m <- Natural -> Some NatRepr
mkNatRepr Natural
m_n
    , Just LeqProof 1 x
LeqProof <- forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) NatRepr x
m ->
      forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall a b. (a -> b) -> a -> b
$ forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr x
m
  SApp [Item [SExp]
"_", Item [SExp]
"FloatingPoint", SAtom (Text -> String
Text.unpack -> String
eb_str), SAtom (Text -> String
Text.unpack -> String
sb_str)]
    | [(Natural
eb_n, String
"")] <- forall a. (Eq a, Num a) => ReadS a
readDec String
eb_str
    , Some NatRepr x
eb <- Natural -> Some NatRepr
mkNatRepr Natural
eb_n
    , Just LeqProof 2 x
LeqProof <- forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @2) NatRepr x
eb
    , [(Natural
sb_n, String
"")] <- forall a. (Eq a, Num a) => ReadS a
readDec String
sb_str
    , Some NatRepr x
sb <- Natural -> Some NatRepr
mkNatRepr Natural
sb_n
    , Just LeqProof 2 x
LeqProof <- forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @2) NatRepr x
sb ->
      forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall a b. (a -> b) -> a -> b
$ forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr forall a b. (a -> b) -> a -> b
$ forall (eb :: Natural) (sb :: Natural).
(2 <= eb, 2 <= sb) =>
NatRepr eb
-> NatRepr sb -> FloatPrecisionRepr ('FloatingPointPrecision eb sb)
FloatingPointPrecisionRepr NatRepr x
eb NatRepr x
sb
  SApp [Item [SExp]
"Array", Item [SExp]
idx_tp_sexp, Item [SExp]
val_tp_sexp] -> do
    Some BaseTypeRepr x
idx_tp <- SExp -> IO (Some BaseTypeRepr)
parseType Item [SExp]
idx_tp_sexp
    Some BaseTypeRepr x
val_tp <- SExp -> IO (Some BaseTypeRepr)
parseType Item [SExp]
val_tp_sexp
    forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall a b. (a -> b) -> a -> b
$ forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
BaseArrayRepr (forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton BaseTypeRepr x
idx_tp) BaseTypeRepr x
val_tp
  SExp
_ -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"unexpected type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExp
sexp


-- | Stores a NatRepr along with proof that its type parameter is a bitvector of
-- that length. Used for easy pattern matching on the LHS of a binding in a
-- do-expression to extract the proof.
data BVProof tp where
  BVProof :: forall n . (1 <= n) => NatRepr n -> BVProof (BaseBVType n)

-- | Given an expression, monadically either returns proof that it is a
-- bitvector or throws an error.
getBVProof :: (I.IsExpr ex, MonadError String m) => ex tp -> m (BVProof tp)
getBVProof :: forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof ex tp
expr = case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
I.exprType ex tp
expr of
  BaseBVRepr NatRepr w
n -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (arg1 :: Natural).
(1 <= arg1) =>
NatRepr arg1 -> BVProof (BaseBVType arg1)
BVProof NatRepr w
n
  BaseTypeRepr tp
t -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"expected BV, found " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BaseTypeRepr tp
t

-- | Operator type descriptions for parsing s-expression of
-- the form @(operator operands ...)@.
--
-- Code is copy-pasted and adapted from `What4.Serialize.Parser`, see
-- <https://github.com/GaloisInc/what4/issues/228>
data Op sym where
    -- | Generic unary operator description.
    Op1 ::
      Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1) ->
      (sym -> I.SymExpr sym arg1 -> IO (I.SymExpr sym ret)) ->
      Op sym
    -- | Generic binary operator description.
    Op2 ::
      Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1 Ctx.::> arg2) ->
      Maybe Assoc ->
      (sym -> I.SymExpr sym arg1 -> I.SymExpr sym arg2 -> IO (I.SymExpr sym ret)) ->
      Op sym
    -- | Encapsulating type for a unary operation that takes one bitvector and
    -- returns another (in IO).
    BVOp1 ::
      (forall w . (1 <= w) => sym -> I.SymBV sym w -> IO (I.SymBV sym w)) ->
      Op sym
    -- | Binop with a bitvector return type, e.g., addition or bitwise operations.
    BVOp2 ::
      Maybe Assoc ->
      (forall w . (1 <= w) => sym -> I.SymBV sym w -> I.SymBV sym w -> IO (I.SymBV sym w)) ->
      Op sym
    -- | Bitvector binop with a boolean return type, i.e., comparison operators.
    BVComp2 ::
      (forall w . (1 <= w) => sym -> I.SymBV sym w -> I.SymBV sym w -> IO (I.Pred sym)) ->
      Op sym

data Assoc = RightAssoc | LeftAssoc

newtype Processor sym a = Processor (ExceptT String (ReaderT (ProcessorEnv sym) IO) a)
  deriving (forall a b. a -> Processor sym b -> Processor sym a
forall a b. (a -> b) -> Processor sym a -> Processor sym b
forall sym a b. a -> Processor sym b -> Processor sym a
forall sym a b. (a -> b) -> Processor sym a -> Processor sym b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Processor sym b -> Processor sym a
$c<$ :: forall sym a b. a -> Processor sym b -> Processor sym a
fmap :: forall a b. (a -> b) -> Processor sym a -> Processor sym b
$cfmap :: forall sym a b. (a -> b) -> Processor sym a -> Processor sym b
Functor, forall sym. Functor (Processor sym)
forall a. a -> Processor sym a
forall sym a. a -> Processor sym a
forall a b. Processor sym a -> Processor sym b -> Processor sym a
forall a b. Processor sym a -> Processor sym b -> Processor sym b
forall a b.
Processor sym (a -> b) -> Processor sym a -> Processor sym b
forall sym a b.
Processor sym a -> Processor sym b -> Processor sym a
forall sym a b.
Processor sym a -> Processor sym b -> Processor sym b
forall sym a b.
Processor sym (a -> b) -> Processor sym a -> Processor sym b
forall a b c.
(a -> b -> c)
-> Processor sym a -> Processor sym b -> Processor sym c
forall sym a b c.
(a -> b -> c)
-> Processor sym a -> Processor sym b -> Processor sym c
forall (f :: Type -> Type).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. Processor sym a -> Processor sym b -> Processor sym a
$c<* :: forall sym a b.
Processor sym a -> Processor sym b -> Processor sym a
*> :: forall a b. Processor sym a -> Processor sym b -> Processor sym b
$c*> :: forall sym a b.
Processor sym a -> Processor sym b -> Processor sym b
liftA2 :: forall a b c.
(a -> b -> c)
-> Processor sym a -> Processor sym b -> Processor sym c
$cliftA2 :: forall sym a b c.
(a -> b -> c)
-> Processor sym a -> Processor sym b -> Processor sym c
<*> :: forall a b.
Processor sym (a -> b) -> Processor sym a -> Processor sym b
$c<*> :: forall sym a b.
Processor sym (a -> b) -> Processor sym a -> Processor sym b
pure :: forall a. a -> Processor sym a
$cpure :: forall sym a. a -> Processor sym a
Applicative, forall sym. Applicative (Processor sym)
forall a. a -> Processor sym a
forall sym a. a -> Processor sym a
forall a b. Processor sym a -> Processor sym b -> Processor sym b
forall a b.
Processor sym a -> (a -> Processor sym b) -> Processor sym b
forall sym a b.
Processor sym a -> Processor sym b -> Processor sym b
forall sym a b.
Processor sym a -> (a -> Processor sym b) -> Processor sym b
forall (m :: Type -> Type).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> Processor sym a
$creturn :: forall sym a. a -> Processor sym a
>> :: forall a b. Processor sym a -> Processor sym b -> Processor sym b
$c>> :: forall sym a b.
Processor sym a -> Processor sym b -> Processor sym b
>>= :: forall a b.
Processor sym a -> (a -> Processor sym b) -> Processor sym b
$c>>= :: forall sym a b.
Processor sym a -> (a -> Processor sym b) -> Processor sym b
Monad, forall sym. Monad (Processor sym)
forall a. IO a -> Processor sym a
forall sym a. IO a -> Processor sym a
forall (m :: Type -> Type).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> Processor sym a
$cliftIO :: forall sym a. IO a -> Processor sym a
MonadIO, MonadError String, MonadReader (ProcessorEnv sym))

data ProcessorEnv sym = ProcessorEnv
  { forall sym. ProcessorEnv sym -> sym
procSym :: sym
  , forall sym. ProcessorEnv sym -> HashMap Text (Some (SymExpr sym))
procLetEnv :: HashMap Text (Some (I.SymExpr sym))
  }

runProcessor :: ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor :: forall sym a.
ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor ProcessorEnv sym
env (Processor ExceptT String (ReaderT (ProcessorEnv sym) IO) a
action) = forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT String (ReaderT (ProcessorEnv sym) IO) a
action) ProcessorEnv sym
env

opTable :: I.IsSymExprBuilder sym => HashMap Text (Op sym)
opTable :: forall sym. IsSymExprBuilder sym => HashMap Text (Op sym)
opTable = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList
  -- Boolean ops
  [ (Text
"not", forall (arg1 :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr (EmptyCtx ::> arg1)
-> (sym -> SymExpr sym arg1 -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
I.notPred)
  , (Text
"=>", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (forall a. a -> Maybe a
Just Assoc
RightAssoc) forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
I.impliesPred)
  , (Text
"and", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
I.andPred)
  , (Text
"or", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
I.orPred)
  , (Text
"xor", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
I.xorPred)
  -- Integer ops
  , (Text
"-", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
I.intSub)
  , (Text
"+", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
I.intAdd)
  , (Text
"*", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
I.intMul)
  , (Text
"div", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
I.intDiv)
  , (Text
"mod", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a. Maybe a
Nothing forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
I.intMod)
  , (Text
"abs", forall (arg1 :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr (EmptyCtx ::> arg1)
-> (sym -> SymExpr sym arg1 -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
I.intAbs)
  , (Text
"<=", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a. Maybe a
Nothing forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
I.intLe)
  , (Text
"<", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a. Maybe a
Nothing forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
I.intLt)
  , (Text
">=", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym 'BaseIntegerType
arg1 SymExpr sym 'BaseIntegerType
arg2 -> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
I.intLe sym
sym SymExpr sym 'BaseIntegerType
arg2 SymExpr sym 'BaseIntegerType
arg1)
  , (Text
">", forall (arg1 :: BaseType) (arg2 :: BaseType) sym (ret :: BaseType).
Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
-> Maybe Assoc
-> (sym
    -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym 'BaseIntegerType
arg1 SymExpr sym 'BaseIntegerType
arg2 -> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
I.intLt sym
sym SymExpr sym 'BaseIntegerType
arg2 SymExpr sym 'BaseIntegerType
arg1)
  -- Bitvector ops
  , (Text
"bvnot", forall sym.
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp1 forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
I.bvNotBits)
  , (Text
"bvneg", forall sym.
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp1 forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
I.bvNeg)
  , (Text
"bvand", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvAndBits)
  , (Text
"bvor", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvOrBits)
  , (Text
"bvxor", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvXorBits)
  , (Text
"bvadd", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvAdd)
  , (Text
"bvsub", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvSub)
  , (Text
"bvmul", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 (forall a. a -> Maybe a
Just Assoc
LeftAssoc) forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvMul)
  , (Text
"bvudiv", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a. Maybe a
Nothing forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvUdiv)
  , (Text
"bvurem", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a. Maybe a
Nothing forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvUrem)
  , (Text
"bvshl", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a. Maybe a
Nothing forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvShl)
  , (Text
"bvlshr", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a. Maybe a
Nothing forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvLshr)
  , (Text
"bvsdiv", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a. Maybe a
Nothing forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvSdiv)
  , (Text
"bvsrem", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a. Maybe a
Nothing forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvSrem)
  , (Text
"bvashr", forall sym.
Maybe Assoc
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a. Maybe a
Nothing forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvAshr)
  , (Text
"bvult", forall sym.
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
I.bvUlt)
  , (Text
"bvule", forall sym.
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
I.bvUle)
  , (Text
"bvugt", forall sym.
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
I.bvUgt)
  , (Text
"bvuge", forall sym.
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
I.bvUge)
  , (Text
"bvslt", forall sym.
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
I.bvSlt)
  , (Text
"bvsle", forall sym.
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
I.bvSle)
  , (Text
"bvsgt", forall sym.
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
I.bvSgt)
  , (Text
"bvsge", forall sym.
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
I.bvSge)
  ]

parseExpr ::
  forall sym . I.IsSymExprBuilder sym => sym -> SExp -> Processor sym (Some (I.SymExpr sym))
parseExpr :: forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym SExp
sexp = case SExp
sexp of
  SExp
"true" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Pred sym
I.truePred sym
sym
  SExp
"false" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Pred sym
I.falsePred sym
sym
  SExp
_ | Just Integer
i <- forall (m :: Type -> Type). MonadFail m => SExp -> m Integer
parseIntSolverValue SExp
sexp ->
      forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
I.intLit sym
sym Integer
i
    | Just (Pair NatRepr tp
w BV tp
bv) <- SExp -> Maybe (Pair NatRepr BV)
parseBVLitHelper SExp
sexp
    , Just LeqProof 1 tp
LeqProof <- forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) NatRepr tp
w ->
      forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
I.bvLit sym
sym NatRepr tp
w BV tp
bv
  SAtom Text
nm -> do
    HashMap Text (Some (SymExpr sym))
env <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks forall sym. ProcessorEnv sym -> HashMap Text (Some (SymExpr sym))
procLetEnv
    case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup Text
nm HashMap Text (Some (SymExpr sym))
env of
      Just Some (SymExpr sym)
expr -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Some (SymExpr sym)
expr
      Maybe (Some (SymExpr sym))
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
""
  SApp [Item [SExp]
"let", SApp [SExp]
bindings_sexp, Item [SExp]
body_sexp] -> do
    HashMap Text (Some (SymExpr sym))
let_env <- forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM
      (\case
        SApp [SAtom Text
nm, Item [SExp]
expr_sexp] -> do
          Some SymExpr sym x
expr <- forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym Item [SExp]
expr_sexp
          forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text
nm, forall k (f :: k -> Type) (x :: k). f x -> Some f
Some SymExpr sym x
expr)
        SExp
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"")
      [SExp]
bindings_sexp
    forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (\ProcessorEnv sym
prov_env -> ProcessorEnv sym
prov_env { procLetEnv :: HashMap Text (Some (SymExpr sym))
procLetEnv = forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
HashMap.union HashMap Text (Some (SymExpr sym))
let_env (forall sym. ProcessorEnv sym -> HashMap Text (Some (SymExpr sym))
procLetEnv ProcessorEnv sym
prov_env) }) forall a b. (a -> b) -> a -> b
$
      forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym Item [SExp]
body_sexp
  SApp [Item [SExp]
"=", Item [SExp]
arg1, Item [SExp]
arg2] -> do
    Some SymExpr sym x
arg1_expr <- forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym Item [SExp]
arg1
    Some SymExpr sym x
arg2_expr <- forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym Item [SExp]
arg2
    case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
I.exprType SymExpr sym x
arg1_expr) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
I.exprType SymExpr sym x
arg2_expr) of
      Just x :~: x
Refl -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
I.isEq sym
sym SymExpr sym x
arg1_expr SymExpr sym x
arg2_expr)
      Maybe (x :~: x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
""
  SApp [Item [SExp]
"ite", Item [SExp]
arg1, Item [SExp]
arg2, Item [SExp]
arg3] -> do
    Some SymExpr sym x
arg1_expr <- forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym Item [SExp]
arg1
    Some SymExpr sym x
arg2_expr <- forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym Item [SExp]
arg2
    Some SymExpr sym x
arg3_expr <- forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym Item [SExp]
arg3
    case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
I.exprType SymExpr sym x
arg1_expr of
      BaseTypeRepr x
I.BaseBoolRepr -> case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
I.exprType SymExpr sym x
arg2_expr) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
I.exprType SymExpr sym x
arg3_expr) of
        Just x :~: x
Refl -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
I.baseTypeIte sym
sym SymExpr sym x
arg1_expr SymExpr sym x
arg2_expr SymExpr sym x
arg3_expr)
        Maybe (x :~: x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
""
      BaseTypeRepr x
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
""
  SApp [Item [SExp]
"concat", Item [SExp]
arg1, Item [SExp]
arg2] -> do
    Some SymExpr sym x
arg1_expr <- forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym Item [SExp]
arg1
    Some SymExpr sym x
arg2_expr <- forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym Item [SExp]
arg2
    BVProof{} <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof SymExpr sym x
arg1_expr
    BVProof{} <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof SymExpr sym x
arg2_expr
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (v :: Natural).
(IsExprBuilder sym, 1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
I.bvConcat sym
sym SymExpr sym x
arg1_expr SymExpr sym x
arg2_expr
  SApp ((SAtom Text
operator) : [SExp]
operands) -> case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup Text
operator (forall sym. IsSymExprBuilder sym => HashMap Text (Op sym)
opTable @sym) of
    Just (Op1 Assignment BaseTypeRepr (EmptyCtx ::> arg1)
arg_types sym -> SymExpr sym arg1 -> IO (SymExpr sym ret)
fn) -> do
      [Some (SymExpr sym)]
args <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym) [SExp]
operands
      forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment BaseTypeRepr (EmptyCtx ::> arg1)
arg_types [Some (SymExpr sym)]
args forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Assignment (SymExpr sym) ctx
Ctx.Empty Ctx.:> SymExpr sym tp
arg1 ->
          forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymExpr sym arg1 -> IO (SymExpr sym ret)
fn sym
sym SymExpr sym tp
arg1)
    Just (Op2 Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
arg_types Maybe Assoc
_ sym -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret)
fn) -> do
      [Some (SymExpr sym)]
args <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym) [SExp]
operands
      forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment BaseTypeRepr ((EmptyCtx ::> arg1) ::> arg2)
arg_types [Some (SymExpr sym)]
args forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Assignment (SymExpr sym) ctx
Ctx.Empty Ctx.:> SymExpr sym tp
arg1 Ctx.:> SymExpr sym tp
arg2 ->
            forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret)
fn sym
sym SymExpr sym tp
arg1 SymExpr sym tp
arg2)
    Just (BVOp1 forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
op) -> do
      Some SymExpr sym x
arg_expr <- forall sym.
IsSymExprBuilder sym =>
sym -> [SExp] -> Processor sym (Some (SymExpr sym))
readOneArg sym
sym [SExp]
operands
      BVProof{} <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof SymExpr sym x
arg_expr
      forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
op sym
sym SymExpr sym x
arg_expr
    Just (BVOp2 Maybe Assoc
_ forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
op) -> do
      (Some SymExpr sym x
arg1, Some SymExpr sym x
arg2) <- forall sym.
IsSymExprBuilder sym =>
sym
-> [SExp] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs sym
sym [SExp]
operands
      BVProof NatRepr n
m <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 1: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof SymExpr sym x
arg1
      BVProof NatRepr n
n <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 2: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof SymExpr sym x
arg2
      case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr n
m NatRepr n
n of
        Just n :~: n
Refl -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
op sym
sym SymExpr sym x
arg1 SymExpr sym x
arg2)
        Maybe (n :~: n)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf "arguments to %s must be the same length, \
                                       \but arg 1 has length %s \
                                       \and arg 2 has length %s"
                                       Text
operator
                                       (forall a. Show a => a -> String
show NatRepr n
m)
                                       (forall a. Show a => a -> String
show NatRepr n
n)
    Just (BVComp2 forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
op) -> do
      (Some SymExpr sym x
arg1, Some SymExpr sym x
arg2) <- forall sym.
IsSymExprBuilder sym =>
sym
-> [SExp] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs sym
sym [SExp]
operands
      BVProof NatRepr n
m <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 1: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof SymExpr sym x
arg1
      BVProof NatRepr n
n <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 2: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof SymExpr sym x
arg2
      case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr n
m NatRepr n
n of
        Just n :~: n
Refl -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
op sym
sym SymExpr sym x
arg1 SymExpr sym x
arg2)
        Maybe (n :~: n)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf "arguments to %s must be the same length, \
                                       \but arg 1 has length %s \
                                       \and arg 2 has length %s"
                                       Text
operator
                                       (forall a. Show a => a -> String
show NatRepr n
m)
                                       (forall a. Show a => a -> String
show NatRepr n
n)
    Maybe (Op sym)
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
""
  SExp
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
""
-- | Verify a list of arguments has a single argument and
-- return it, else raise an error.
readOneArg ::
  I.IsSymExprBuilder sym
  => sym
  -> [SExp]
  -> Processor sym (Some (I.SymExpr sym))
readOneArg :: forall sym.
IsSymExprBuilder sym =>
sym -> [SExp] -> Processor sym (Some (SymExpr sym))
readOneArg sym
sym [SExp]
operands = do
  [Some (SymExpr sym)]
args <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym) [SExp]
operands
  case [Some (SymExpr sym)]
args of
    [Item [Some (SymExpr sym)]
arg] -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Item [Some (SymExpr sym)]
arg
    [Some (SymExpr sym)]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"expecting 1 argument, got %d" (forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some (SymExpr sym)]
args)

-- | Verify a list of arguments has two arguments and return
-- it, else raise an error.
readTwoArgs ::
  I.IsSymExprBuilder sym
  => sym
  ->[SExp]
  -> Processor sym (Some (I.SymExpr sym), Some (I.SymExpr sym))
readTwoArgs :: forall sym.
IsSymExprBuilder sym =>
sym
-> [SExp] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs sym
sym [SExp]
operands = do
  [Some (SymExpr sym)]
args <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
IsSymExprBuilder sym =>
sym -> SExp -> Processor sym (Some (SymExpr sym))
parseExpr sym
sym) [SExp]
operands
  case [Some (SymExpr sym)]
args of
    [Item [Some (SymExpr sym)]
arg1, Item [Some (SymExpr sym)]
arg2] -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (Item [Some (SymExpr sym)]
arg1, Item [Some (SymExpr sym)]
arg2)
    [Some (SymExpr sym)]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"expecting 2 arguments, got %d" (forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some (SymExpr sym)]
args)

exprAssignment ::
  forall sym ctx ex . (I.IsSymExprBuilder sym, I.IsExpr ex)
  => Ctx.Assignment BaseTypeRepr ctx
  -> [Some ex]
  -> Processor sym (Ctx.Assignment ex ctx)
exprAssignment :: forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment BaseTypeRepr ctx
tpAssns [Some ex]
exs = do
  Some Assignment ex x
exsAsn <- forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList [Some ex]
exs
  Assignment BaseTypeRepr x
exsRepr <- forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
I.exprType Assignment ex x
exsAsn
  case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Assignment BaseTypeRepr x
exsRepr Assignment BaseTypeRepr ctx
tpAssns of
    Just x :~: ctx
Refl -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Assignment ex x
exsAsn
    Maybe (x :~: ctx)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
      String
"Unexpected expression types for " -- ++ show exsAsn
      forall a. [a] -> [a] -> [a]
++ String
"\nExpected: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Assignment BaseTypeRepr ctx
tpAssns
      forall a. [a] -> [a] -> [a]
++ String
"\nGot: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Assignment BaseTypeRepr x
exsRepr

-- | Utility function for contextualizing errors. Prepends the given prefix
-- whenever an error is thrown.
prefixError :: (Monoid e, MonadError e m) => e -> m a -> m a
prefixError :: forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError e
prefix m a
act = forall e (m :: Type -> Type) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError m a
act (forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => a -> a -> a
mappend e
prefix)


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

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

-- | Get a value from a solver (must be called after checkSat)
runGetValue :: SMTLib2Tweaks a
            => Session t a
            -> Term
            -> IO SExp
runGetValue :: forall a t. SMTLib2Tweaks a => Session t a -> Term -> IO SExp
runGetValue Session t a
s Term
e = do
  forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> [Term] -> IO ()
writeGetValue (forall t a. Session t a -> WriterConn t (Writer a)
sessionWriter Session t a
s) [ Term
e ]
  let valRsp :: SMTResponse -> Maybe SExp
valRsp = \case
        AckSuccessSExp (SApp [SApp [Item [SExp]
_, Item [SExp]
b]]) -> forall a. a -> Maybe a
Just Item [SExp]
b
        SMTResponse
_ -> forall a. Maybe a
Nothing
  forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
"get value" SMTResponse -> Maybe SExp
valRsp (forall t a. Session t a -> WriterConn t (Writer a)
sessionWriter Session t a
s) ([Term] -> Command
SMT2.getValue [Term
e])

-- | runGetAbducts s nm p n, returns n formulas (as strings) the disjunction of which entails p (along with all
--   the assertions in the context)
runGetAbducts :: SMTLib2Tweaks a
             => Session t a
             -> Int
             -> Text
             -> Term
             -> IO [String]
runGetAbducts :: forall a t.
SMTLib2Tweaks a =>
Session t a -> Int -> Text -> Term -> IO [String]
runGetAbducts Session t a
s Int
n Text
nm Term
p = 
  if (Int
n forall a. Ord a => a -> a -> Bool
> Int
0) then do
    forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Term -> IO ()
writeGetAbduct (forall t a. Session t a -> WriterConn t (Writer a)
sessionWriter Session t a
s) Text
nm Term
p
    let valRsp :: SMTResponse -> Maybe String
valRsp = \SMTResponse
x -> case SMTResponse
x of
          -- SMT solver returns `(define-fun nm () Bool X)` where X is the abduct, we discard everything but the abduct
          AckSuccessSExp (SApp (SExp
_ : SExp
_ : SExp
_ : SExp
_ : [SExp]
abduct)) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [String] -> String
Data.String.unwords (forall a b. (a -> b) -> [a] -> [b]
map SExp -> String
sExpToString [SExp]
abduct)
          SMTResponse
_ -> forall a. Maybe a
Nothing
    -- get first abduct using the get-abduct command
    String
abd1 <- forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
"get abduct" SMTResponse -> Maybe String
valRsp (forall t a. Session t a -> WriterConn t (Writer a)
sessionWriter Session t a
s) (Text -> Term -> Command
SMT2.getAbduct Text
nm Term
p)
    if (Int
n forall a. Ord a => a -> a -> Bool
> Int
1) then do
      let rest :: Int
rest = Int
n forall a. Num a => a -> a -> a
- Int
1
      forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m ()
replicateM_ Int
rest forall a b. (a -> b) -> a -> b
$ forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeGetAbductNext (forall t a. Session t a -> WriterConn t (Writer a)
sessionWriter Session t a
s)
      -- get the rest of the abducts using the get-abduct-next command
      [String]
abdRest <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int
1..Int
rest] forall a b. (a -> b) -> a -> b
$ \Int
_ -> forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
"get abduct next" SMTResponse -> Maybe String
valRsp (forall t a. Session t a -> WriterConn t (Writer a)
sessionWriter Session t a
s) (Text -> Term -> Command
SMT2.getAbduct Text
nm Term
p)
      forall (m :: Type -> Type) a. Monad m => a -> m a
return (String
abd1forall a. a -> [a] -> [a]
:[String]
abdRest)
    else forall (m :: Type -> Type) a. Monad m => a -> m a
return [String
abd1]
  else forall (m :: Type -> Type) a. Monad m => a -> m a
return []

-- | 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 :: forall b t a.
SMTLib2Tweaks b =>
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 = forall t a. Session t a -> WriterConn t (Writer a)
sessionWriter Session t b
s
         r :: InputStream Text
r = forall t a. Session t a -> InputStream Text
sessionResponse Session t b
s
     forall h t. SMTWriter h => WriterConn t h -> [Command h] -> IO ()
addCommands WriterConn t (Writer b)
w (forall h (f :: Type -> Type). SMTWriter h => f h -> [Command h]
checkCommands WriterConn t (Writer b)
w)
     SatResult () ()
res <- forall h (f :: Type -> Type) t.
SMTReadWriter h =>
f h -> WriterConn t h -> IO (SatResult () ())
smtSatResult WriterConn t (Writer b)
w WriterConn t (Writer b)
w
     case SatResult () ()
res of
       Unsat ()
x -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
doEval (forall mdl core. core -> SatResult mdl core
Unsat ()
x)
       SatResult () ()
Unknown -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
doEval forall mdl core. SatResult mdl core
Unknown
       Sat ()
_ ->
         do GroundEvalFn t
evalFn <- forall t h.
SMTWriter h =>
WriterConn t h -> SMTEvalFunctions h -> IO (GroundEvalFn t)
smtExprGroundEvalFn WriterConn t (Writer b)
w (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 (forall mdl core. mdl -> SatResult mdl core
Sat (GroundEvalFn t
evalFn, forall a. Maybe a
Nothing))

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

  smtSatResult :: forall (f :: Type -> Type) t.
f (Writer a) -> WriterConn t (Writer a) -> IO (SatResult () ())
smtSatResult f (Writer a)
p WriterConn t (Writer a)
s =
    let satRsp :: SMTResponse -> Maybe (SatResult () ())
satRsp = \case
          SMTResponse
AckSat     -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall mdl core. mdl -> SatResult mdl core
Sat ()
          SMTResponse
AckUnsat   -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall mdl core. core -> SatResult mdl core
Unsat ()
          SMTResponse
AckUnknown -> forall a. a -> Maybe a
Just forall mdl core. SatResult mdl core
Unknown
          SMTResponse
_ -> forall a. Maybe a
Nothing
    in forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
"sat result" SMTResponse -> Maybe (SatResult () ())
satRsp WriterConn t (Writer a)
s
       (forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall h (f :: Type -> Type). SMTWriter h => f h -> [Command h]
checkCommands f (Writer a)
p)

  smtUnsatAssumptionsResult :: forall (f :: Type -> Type) t.
f (Writer a) -> WriterConn t (Writer a) -> IO [(Bool, Text)]
smtUnsatAssumptionsResult f (Writer a)
p WriterConn t (Writer a)
s =
    let unsatAssumpRsp :: SMTResponse -> Maybe [(Bool, Text)]
unsatAssumpRsp = \case
         AckSuccessSExp (SExp -> Maybe [(Bool, Text)]
asNegAtomList -> Just [(Bool, Text)]
as) -> forall a. a -> Maybe a
Just [(Bool, Text)]
as
         SMTResponse
_ -> forall a. Maybe a
Nothing
        cmd :: Command (Writer a)
cmd = forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
getUnsatAssumptionsCommand f (Writer a)
p
    in forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
"unsat assumptions" SMTResponse -> Maybe [(Bool, Text)]
unsatAssumpRsp WriterConn t (Writer a)
s Command (Writer a)
cmd

  smtUnsatCoreResult :: forall (f :: Type -> Type) t.
f (Writer a) -> WriterConn t (Writer a) -> IO [Text]
smtUnsatCoreResult f (Writer a)
p WriterConn t (Writer a)
s =
    let unsatCoreRsp :: SMTResponse -> Maybe [Text]
unsatCoreRsp = \case
          AckSuccessSExp (SExp -> Maybe [Text]
asAtomList -> Just [Text]
nms) -> forall a. a -> Maybe a
Just [Text]
nms
          SMTResponse
_ -> forall a. Maybe a
Nothing
        cmd :: Command (Writer a)
cmd = forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
getUnsatCoreCommand f (Writer a)
p
    in forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
"unsat core" SMTResponse -> Maybe [Text]
unsatCoreRsp WriterConn t (Writer a)
s Command (Writer a)
cmd

  smtAbductResult :: forall (f :: Type -> Type) t.
f (Writer a)
-> WriterConn t (Writer a) -> Text -> Term (Writer a) -> IO String
smtAbductResult f (Writer a)
p WriterConn t (Writer a)
s Text
nm Term (Writer a)
t =
    let abductRsp :: SMTResponse -> Maybe String
abductRsp = \case
          AckSuccessSExp (SApp (SExp
_ : SExp
_ : SExp
_ : SExp
_ : [SExp]
abduct)) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [String] -> String
Data.String.unwords (forall a b. (a -> b) -> [a] -> [b]
map SExp -> String
sExpToString [SExp]
abduct)
          SMTResponse
_ -> forall a. Maybe a
Nothing
        cmd :: Command (Writer a)
cmd = forall h (f :: Type -> Type).
SMTWriter h =>
f h -> Text -> Term h -> Command h
getAbductCommand f (Writer a)
p Text
nm Term (Writer a)
t
    in forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
"get abduct" SMTResponse -> Maybe String
abductRsp WriterConn t (Writer a)
s Command (Writer a)
cmd

  smtAbductNextResult :: forall (f :: Type -> Type) t.
f (Writer a) -> WriterConn t (Writer a) -> IO String
smtAbductNextResult f (Writer a)
p WriterConn t (Writer a)
s =
    let abductRsp :: SMTResponse -> Maybe String
abductRsp = \case
          AckSuccessSExp (SApp (SExp
_ : SExp
_ : SExp
_ : SExp
_ : [SExp]
abduct)) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [String] -> String
Data.String.unwords (forall a b. (a -> b) -> [a] -> [b]
map SExp -> String
sExpToString [SExp]
abduct)
          SMTResponse
_ -> forall a. Maybe a
Nothing
        cmd :: Command (Writer a)
cmd = forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
getAbductNextCommand f (Writer a)
p
    in forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
"get abduct next" SMTResponse -> Maybe String
abductRsp WriterConn t (Writer a)
s Command (Writer a)
cmd


smtAckResult :: AcknowledgementAction t (Writer a)
smtAckResult :: forall t a. AcknowledgementAction t (Writer a)
smtAckResult = forall t h.
(WriterConn t h -> Command h -> IO ()) -> AcknowledgementAction t h
AckAction forall a b. (a -> b) -> a -> b
$ forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
"get ack" forall a b. (a -> b) -> a -> b
$ \case
                 SMTResponse
AckSuccess -> forall a. a -> Maybe a
Just ()
                 SMTResponse
_ -> forall a. Maybe a
Nothing


smtLibEvalFuns ::
  forall t a. SMTLib2Tweaks a => Session t a -> SMTEvalFunctions (Writer a)
smtLibEvalFuns :: forall t a.
SMTLib2Tweaks a =>
Session t a -> SMTEvalFunctions (Writer a)
smtLibEvalFuns Session t a
s = SMTEvalFunctions
                  { smtEvalBool :: Term (Writer a) -> IO Bool
smtEvalBool = Term -> IO Bool
evalBool
                  , smtEvalBV :: forall (w :: Natural). NatRepr w -> Term (Writer a) -> IO (BV w)
smtEvalBV = forall (w :: Natural). NatRepr w -> Term -> IO (BV w)
evalBV
                  , smtEvalReal :: Term (Writer a) -> IO Rational
smtEvalReal = Term -> 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))
evalFloat
                  , smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper (Writer a))
smtEvalBvArray = forall a. a -> Maybe a
Just (forall h.
(forall (w :: Natural) (v :: Natural). SMTEvalBVArrayFn h w v)
-> SMTEvalBVArrayWrapper h
SMTEvalBVArrayWrapper forall (w :: Natural) (v :: Natural).
SMTEvalBVArrayFn (Writer a) w v
evalBvArray)
                  , smtEvalString :: Term (Writer a) -> IO Text
smtEvalString = Term -> IO Text
evalStr
                  }
  where
  evalBool :: Term -> IO Bool
evalBool Term
tm = forall (m :: Type -> Type). MonadFail m => SExp -> m Bool
parseBoolSolverValue forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 = forall (m :: Type -> Type). MonadFail m => SExp -> m Rational
parseRealSolverValue forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a t. SMTLib2Tweaks a => Session t a -> Term -> IO SExp
runGetValue Session t a
s Term
tm
  evalStr :: Term -> IO Text
evalStr Term
tm = forall (m :: Type -> Type). MonadFail m => SExp -> m Text
parseStringSolverValue forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 :: forall (w :: Natural). NatRepr w -> Term -> IO (BV w)
evalBV NatRepr w
w Term
tm = forall (m :: Type -> Type) (w :: Natural).
MonadFail m =>
NatRepr w -> SExp -> m (BV w)
parseBvSolverValue NatRepr w
w forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> Term -> IO (BV (FloatPrecisionBits fpp))
evalFloat FloatPrecisionRepr fpp
fpp Term
tm = forall (m :: Type -> Type) (fpp :: FloatPrecision).
MonadFail m =>
FloatPrecisionRepr fpp -> SExp -> m (BV (FloatPrecisionBits fpp))
parseFloatSolverValue FloatPrecisionRepr fpp
fpp forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 :: forall (w :: Natural) (v :: Natural).
SMTEvalBVArrayFn (Writer a) w v
evalBvArray NatRepr w
w NatRepr v
v Term (Writer a)
tm = forall (m :: Type -> Type) (w :: Natural) (v :: Natural).
(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 forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a t. SMTLib2Tweaks a => Session t a -> Term -> IO SExp
runGetValue Session t a
s 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) -> IO ErrorBehavior
  getErrorBehavior a
_ WriterConn t (Writer a)
_ = 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 ->
       -- | strictness override configuration
       Maybe (CFG.ConfigOption I.BaseBoolType) ->
       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 Maybe (ConfigOption 'BaseBoolType)
strictOpt ExprBuilder t st fs
sym OutputStream Text
h InputStream Text
in_h = do
    let cfg :: Config
cfg = forall sym. IsExprBuilder sym => sym -> Config
I.getConfiguration ExprBuilder t st fs
sym
    ResponseStrictness
strictness <- Maybe (ConfigOption 'BaseBoolType)
-> ConfigOption 'BaseBoolType -> Config -> IO ResponseStrictness
parserStrictness Maybe (ConfigOption 'BaseBoolType)
strictOpt ConfigOption 'BaseBoolType
strictSMTParsing Config
cfg
    forall a t.
a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> ResponseStrictness
-> 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 ResponseStrictness
strictness (forall a. Show a => a -> String
show a
solver) Bool
True ProblemFeatures
feats Bool
True
      forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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
    -> Maybe (CFG.ConfigOption I.BaseBoolType)
       -- ^ strictness override configuration
    -> 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 Maybe (ConfigOption 'BaseBoolType)
strictOpt ExprBuilder t st fs
sym String
path LogData
logData Session t a -> IO b
action = do
    [String]
args <- forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs a
solver ExprBuilder t st fs
sym
    forall a.
String
-> [String]
-> Maybe String
-> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
-> IO a
withProcessHandles String
path [String]
args forall a. Maybe a
Nothing 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
            (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Handle
x -> (Text
"; ", Handle
x)) forall a b. (a -> b) -> a -> b
$ LogData -> Maybe Handle
logHandle LogData
logData)

        WriterConn t (Writer a)
writer <- forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> Maybe (ConfigOption 'BaseBoolType)
-> ExprBuilder t st fs
-> OutputStream Text
-> InputStream Text
-> IO (WriterConn t (Writer a))
newDefaultWriter a
solver AcknowledgementAction t (Writer a)
ack ProblemFeatures
feats Maybe (ConfigOption 'BaseBoolType)
strictOpt ExprBuilder t st fs
sym OutputStream Text
in_stream InputStream Text
out_stream
        let s :: Session t a
s = 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
        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
        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 -> forall (m :: Type -> Type) a. Monad m => a -> m a
return b
r
          Exit.ExitFailure Int
exit_code -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$
            forall a. Show a => a -> String
show a
solver forall a. [a] -> [a] -> [a]
++ String
" exited with unexpected code: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
exit_code

  runSolverInOverride
    :: a
    -> AcknowledgementAction t (Writer a)
    -> ProblemFeatures
    -> Maybe (CFG.ConfigOption I.BaseBoolType)
    -- ^ strictness override configuration
    -> 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 Maybe (ConfigOption 'BaseBoolType)
strictOpt ExprBuilder t st fs
sym LogData
logData [BoolExpr t]
predicates SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b
cont = do
    forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
I.logSolverEvent ExprBuilder t st fs
sym
      (SolverStartSATQuery -> SolverEvent
I.SolverStartSATQuery forall a b. (a -> b) -> a -> b
$ I.SolverStartSATQueryRec
        { satQuerySolverName :: String
I.satQuerySolverName = forall a. Show a => a -> String
show a
solver
        , satQueryReason :: String
I.satQueryReason     = LogData -> String
logReason LogData
logData
        })
    String
path <- forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a -> ExprBuilder t st fs -> IO String
defaultSolverPath a
solver ExprBuilder t st fs
sym
    forall a t (st :: Type -> Type) fs b.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> Maybe (ConfigOption 'BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t a -> IO b)
-> IO b
withSolver a
solver AcknowledgementAction t (Writer a)
ack ProblemFeatures
feats Maybe (ConfigOption 'BaseBoolType)
strictOpt ExprBuilder t st fs
sym String
path (LogData
logData{logVerbosity :: Int
logVerbosity=Int
2}) forall a b. (a -> b) -> a -> b
$ \Session t a
session -> do
      -- Assume the predicates hold.
      forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [BoolExpr t]
predicates (forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMTWriter.assume (forall t a. Session t a -> WriterConn t (Writer a)
sessionWriter Session t a
session))
      -- Run check SAT and get the model back.
      forall b t a.
SMTLib2Tweaks b =>
Session t b
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runCheckSat Session t a
session forall a b. (a -> b) -> a -> b
$ \SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
result -> do
        forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
I.logSolverEvent ExprBuilder t st fs
sym
          (SolverEndSATQuery -> SolverEvent
I.SolverEndSATQuery forall a b. (a -> b) -> a -> b
$ I.SolverEndSATQueryRec
            { satQueryResult :: SatResult () ()
I.satQueryResult = forall a b. SatResult a b -> SatResult () ()
forgetModelAndCore SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
result
            , satQueryError :: Maybe String
I.satQueryError  = 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
                 -> Maybe (CFG.ConfigOption I.BaseBoolType)
                    -- ^ strictness override configuration
                 -> B.ExprBuilder t st fs
                 -> IO.Handle
                 -> [B.BoolExpr t]
                 -> IO ()
writeDefaultSMT2 :: forall a t (st :: Type -> Type) fs.
SMTLib2Tweaks a =>
a
-> String
-> ProblemFeatures
-> Maybe (ConfigOption 'BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
writeDefaultSMT2 a
a String
nm ProblemFeatures
feat Maybe (ConfigOption 'BaseBoolType)
strictOpt ExprBuilder t st fs
sym Handle
h [BoolExpr t]
ps = do
  WriterConn t (Writer a)
c <- forall a t (st :: Type -> Type) fs.
SMTLib2Tweaks a =>
a
-> String
-> ProblemFeatures
-> Maybe (ConfigOption 'BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> IO (WriterConn t (Writer a))
defaultFileWriter a
a String
nm ProblemFeatures
feat Maybe (ConfigOption 'BaseBoolType)
strictOpt ExprBuilder t st fs
sym Handle
h
  forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
setProduceModels WriterConn t (Writer a)
c Bool
True
  forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [BoolExpr t]
ps (forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMTWriter.assume WriterConn t (Writer a)
c)
  forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeCheckSat WriterConn t (Writer a)
c
  forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeExit WriterConn t (Writer a)
c

defaultFileWriter ::
  SMTLib2Tweaks a =>
  a ->
  String ->
  ProblemFeatures ->
  Maybe (CFG.ConfigOption I.BaseBoolType) ->
  B.ExprBuilder t st fs ->
  IO.Handle ->
  IO (WriterConn t (Writer a))
defaultFileWriter :: forall a t (st :: Type -> Type) fs.
SMTLib2Tweaks a =>
a
-> String
-> ProblemFeatures
-> Maybe (ConfigOption 'BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> IO (WriterConn t (Writer a))
defaultFileWriter a
a String
nm ProblemFeatures
feat Maybe (ConfigOption 'BaseBoolType)
strictOpt ExprBuilder t st fs
sym Handle
h = do
  SymbolVarBimap t
bindings <- 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 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 <- forall a. IO (InputStream a)
Streams.nullInput
  let cfg :: Config
cfg = forall sym. IsExprBuilder sym => sym -> Config
I.getConfiguration ExprBuilder t st fs
sym
  ResponseStrictness
strictness <- Maybe (ConfigOption 'BaseBoolType)
-> ConfigOption 'BaseBoolType -> Config -> IO ResponseStrictness
parserStrictness Maybe (ConfigOption 'BaseBoolType)
strictOpt ConfigOption 'BaseBoolType
strictSMTParsing Config
cfg
  forall a t.
a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> ResponseStrictness
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
newWriter a
a OutputStream Text
str InputStream Text
null_in forall t h. AcknowledgementAction t h
nullAcknowledgementAction ResponseStrictness
strictness String
nm Bool
True ProblemFeatures
feat Bool
True SymbolVarBimap t
bindings

-- n.b. commonly used for the startSolverProcess method of the
-- OnlineSolver class, so it's helpful for the type suffixes to align
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
  -> SolverGoalTimeout
  -> ProblemFeatures
  -> Maybe (CFG.ConfigOption I.BaseBoolType)
  -- ^ strictness override configuration
  -> Maybe IO.Handle
  -> B.ExprBuilder t st fs
  -> IO (SolverProcess t (Writer a))
startSolver :: forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> (WriterConn t (Writer a) -> IO ())
-> SolverGoalTimeout
-> ProblemFeatures
-> Maybe (ConfigOption 'BaseBoolType)
-> 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 SolverGoalTimeout
tmout ProblemFeatures
feats Maybe (ConfigOption 'BaseBoolType)
strictOpt Maybe Handle
auxOutput ExprBuilder t st fs
sym = do
  String
path <- 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 <- 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 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
       (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 <- forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> Maybe (ConfigOption 'BaseBoolType)
-> ExprBuilder t st fs
-> OutputStream Text
-> InputStream Text
-> IO (WriterConn t (Writer a))
newDefaultWriter a
solver AcknowledgementAction t (Writer a)
ack ProblemFeatures
feats Maybe (ConfigOption 'BaseBoolType)
strictOpt 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 <- forall a t.
SMTLib2GenericSolver a =>
a -> WriterConn t (Writer a) -> IO ErrorBehavior
getErrorBehavior a
solver WriterConn t (Writer a)
writer

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

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

  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! 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
            , solverStderr :: HandleReader
solverStderr   = HandleReader
err_reader
            , solverHandle :: ProcessHandle
solverHandle   = ProcessHandle
ph
            , solverErrorBehavior :: ErrorBehavior
solverErrorBehavior = ErrorBehavior
errBeh
            , solverEvalFuns :: SMTEvalFunctions (Writer a)
solverEvalFuns = 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    = forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
I.logSolverEvent ExprBuilder t st fs
sym
            , solverName :: String
solverName     = forall a. Show a => a -> String
show a
solver
            , solverEarlyUnsat :: IORef (Maybe Int)
solverEarlyUnsat = IORef (Maybe Int)
earlyUnsatRef
            , solverSupportsResetAssertions :: Bool
solverSupportsResetAssertions = forall a. SMTLib2GenericSolver a => a -> Bool
supportsResetAssertions a
solver
            , solverGoalTimeout :: SolverGoalTimeout
solverGoalTimeout = SolverGoalTimeout
tmout
            }

shutdownSolver
  :: SMTLib2GenericSolver a => a -> SolverProcess t (Writer a) -> IO (Exit.ExitCode, Lazy.Text)
shutdownSolver :: forall a t.
SMTLib2GenericSolver a =>
a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
shutdownSolver a
_solver SolverProcess t (Writer a)
p = do
  -- Tell solver to exit
  forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
writeExit (forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess t (Writer a)
p)
  Text
txt <- HandleReader -> IO Text
readAllLines (forall scope solver. SolverProcess scope solver -> HandleReader
solverStderr SolverProcess t (Writer a)
p)
  HandleReader -> IO ()
stopHandleReader (forall scope solver. SolverProcess scope solver -> HandleReader
solverStderr SolverProcess t (Writer a)
p)
  ExitCode
ec <- forall scope solver. SolverProcess scope solver -> IO ExitCode
solverCleanupCallback SolverProcess t (Writer a)
p
  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 = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList $(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 :: forall ann. SolverVersionCheckError -> Doc ann
ppSolverVersionCheckError SolverVersionCheckError
err =
  forall ann. [Doc ann] -> Doc ann
PP.vsep
  [ Doc ann
"Unexpected error while checking solver version:"
  , case SolverVersionCheckError
err of
      UnparseableVersion ParsingError
parseErr ->
        forall ann. [Doc ann] -> Doc ann
PP.hsep
        [ Doc ann
"Couldn't parse solver version number:"
        , 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 :: forall ann. SolverVersionError -> Doc ann
ppSolverVersionError SolverVersionError
err =
  forall ann. [Doc ann] -> Doc ann
PP.vsep
  [ Doc ann
"Solver did not meet version bound restrictions:"
  , Doc ann
"Lower bound (inclusive):" forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> 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):" forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> forall {a} {ann}. Show a => Maybe a -> Doc ann
na (SolverBounds -> Maybe Version
upper (SolverVersionError -> SolverBounds
vBounds SolverVersionError
err))
  , Doc ann
"Actual version:" forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> 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) = 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 :: WriterConn t a -> IO Text
nameResult :: forall t a. WriterConn t a -> IO Text
nameResult WriterConn t a
conn =
  forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
"solver name"
  (\case
      RspName Text
nm -> forall a. a -> Maybe a
Just Text
nm
      SMTResponse
_ -> forall a. Maybe a
Nothing
  )
  WriterConn t a
conn Command
SMT2.getName


-- | Query the solver's error behavior setting
queryErrorBehavior :: SMTLib2Tweaks a =>
  WriterConn t (Writer a) -> IO ErrorBehavior
queryErrorBehavior :: forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> IO ErrorBehavior
queryErrorBehavior WriterConn t (Writer a)
conn =
  do let cmd :: Command
cmd = Command
SMT2.getErrorBehavior
     forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
writeCommand WriterConn t (Writer a)
conn Command
cmd
     forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
"error behavior"
       (\case
           RspErrBehavior Text
bh -> case Text
bh of
             Text
"continued-execution" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ErrorBehavior
ContinueOnError
             Text
"immediate-exit" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ErrorBehavior
ImmediateExit
             Text
_ -> forall a e. Exception e => e -> a
throw forall a b. (a -> b) -> a -> b
$ Command -> Text -> SMTLib2Exception
SMTLib2ResponseUnrecognized Command
cmd Text
bh
           SMTResponse
_ -> forall a. Maybe a
Nothing
       ) WriterConn t (Writer a)
conn Command
cmd


-- | Get the result of a version query
versionResult :: WriterConn t a -> IO Text
versionResult :: forall t a. WriterConn t a -> IO Text
versionResult WriterConn t a
conn =
  forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
"solver version"
  (\case
      RspVersion Text
v -> forall a. a -> Maybe a
Just Text
v
      SMTResponse
_ -> forall a. Maybe a
Nothing
  )
  WriterConn t a
conn Command
SMT2.getVersion


-- | 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' :: forall solver scope.
SMTLib2Tweaks solver =>
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 = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope (Writer solver)
proc
      name :: String
name = forall t h. WriterConn t h -> String
smtWriterName WriterConn scope (Writer solver)
conn
      done :: IO (Either a (Maybe a))
done = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right forall a. Maybe a
Nothing)
      verr :: SolverBounds -> Version -> f (Either a (Maybe SolverVersionError))
verr SolverBounds
bnds Version
actual = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right (forall a. a -> Maybe a
Just (SolverBounds -> Version -> SolverVersionError
SolverVersionError SolverBounds
bnds Version
actual))) in
  case 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 -> forall {a} {a}. IO (Either a (Maybe a))
done
    Just SolverBounds
bnds ->
      do forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
getVersion WriterConn scope (Writer solver)
conn
         Text
res <- forall t a. WriterConn t a -> IO Text
versionResult forall a b. (a -> b) -> a -> b
$ forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope (Writer solver)
proc
         case Text -> Either ParsingError Version
Versions.version Text
res of
           Left ParsingError
e -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (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) -> forall {a} {a}. IO (Either a (Maybe a))
done
               (Maybe Version
Nothing, Just Version
maxVer) ->
                 if Version
actualVer forall a. Ord a => a -> a -> Bool
< Version
maxVer then forall {a} {a}. IO (Either a (Maybe a))
done else 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 forall a. Ord a => a -> a -> Bool
<= Version
actualVer then forall {a} {a}. IO (Either a (Maybe a))
done else 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 forall a. Ord a => a -> a -> Bool
<= Version
actualVer Bool -> Bool -> Bool
&& Version
actualVer forall a. Ord a => a -> a -> Bool
< Version
maxVer then forall {a} {a}. IO (Either a (Maybe a))
done else 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 :: forall solver scope.
SMTLib2Tweaks solver =>
SolverProcess scope (Writer solver)
-> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
checkSolverVersion = forall solver scope.
SMTLib2Tweaks solver =>
Map Text SolverBounds
-> SolverProcess scope (Writer solver)
-> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
checkSolverVersion' Map Text SolverBounds
defaultSolverBounds