{-# 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
(
Writer
, SMTLib2Tweaks(..)
, newWriter
, writeCheckSat
, writeExit
, writeGetValue
, writeGetAbduct
, writeGetAbductNext
, writeCheckSynth
, runCheckSat
, runGetAbducts
, asSMT2Type
, setOption
, getVersion
, versionResult
, getName
, nameResult
, setProduceModels
, smtLibEvalFuns
, smtlib2Options
, parseFnModel
, parseFnValues
, SMT2.Logic(..)
, SMT2.qf_bv
, SMT2.allSupported
, SMT2.hornLogic
, all_supported
, setLogic
, SMT2.Sort(..)
, SMT2.arraySort
, Term(..)
, arrayConst
, What4.Protocol.SMTLib2.arraySelect
, arrayStore
, Session(..)
, SMTLib2GenericSolver(..)
, writeDefaultSMT2
, defaultFileWriter
, startSolver
, shutdownSolver
, smtAckResult
, SMTLib2Exception(..)
, ppSolverVersionCheckError
, ppSolverVersionError
, checkSolverVersion
, checkSolverVersion'
, queryErrorBehavior
, defaultSolverBounds
, 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
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
data SMTFloatPrecision =
SMTFloatPrecision { SMTFloatPrecision -> Natural
smtFloatExponentBits :: !Natural
, SMTFloatPrecision -> Natural
smtFloatSignificandBits :: !Natural
}
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
")"
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
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
| Char
'\"' forall a. Eq a => a -> a -> Bool
== Char
c = Builder
"\"\"" forall a. Semigroup a => a -> a -> a
<> Builder
x
| Char
'\\' forall a. Eq a => a -> a -> Bool
== Char
c = Builder
"\\u{5c}" forall a. Semigroup a => a -> a -> a
<> Builder
x
| forall {a}. Enum a => a -> Bool
inLiteralRange Char
c = Char -> Builder
Builder.singleton Char
c forall a. Semigroup a => a -> a -> a
<> Builder
x
| 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
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')
| 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')
| 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'''
| (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
class Show a => SMTLib2Tweaks a where
smtlib2tweaks :: a
smtlib2exitCommand :: Maybe SMT2.Command
smtlib2exitCommand = forall a. a -> Maybe a
Just Command
SMT2.exit
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]
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
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)
smtlib2StructProj ::
Int ->
Int ->
Term ->
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
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)
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
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)
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)
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]
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)
newWriter :: a
-> Streams.OutputStream Text
-> Streams.InputStream Text
-> AcknowledgementAction t (Writer a)
-> ResponseStrictness
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> B.SymbolVarBimap t
-> 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)
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)
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
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
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
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
-> Integer
-> 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)
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)
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 + 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)
(NatRepr eb)
(BV.BV eb)
(NatRepr sb)
(BV.BV sb)
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
data BVProof tp where
BVProof :: forall n . (1 <= n) => NatRepr n -> BVProof (BaseBVType n)
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
data Op sym where
Op1 ::
Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1) ->
(sym -> I.SymExpr sym arg1 -> IO (I.SymExpr sym ret)) ->
Op sym
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
BVOp1 ::
(forall w . (1 <= w) => sym -> I.SymBV sym w -> IO (I.SymBV sym w)) ->
Op sym
BVOp2 ::
Maybe Assoc ->
(forall w . (1 <= w) => sym -> I.SymBV sym w -> I.SymBV sym w -> IO (I.SymBV sym w)) ->
Op sym
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
[ (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)
, (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)
, (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
""
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)
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 "
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
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)
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)
}
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 :: 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
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
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)
[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 []
runCheckSat :: forall b t a.
SMTLib2Tweaks b
=> Session t b
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
-> 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 ->
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
withSolver
:: a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> Maybe (CFG.ConfigOption I.BaseBoolType)
-> B.ExprBuilder t st fs
-> FilePath
-> 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 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
}
forall a t.
SMTLib2GenericSolver a =>
WriterConn t (Writer a) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer a)
writer
b
r <- Session t a -> IO b
action Session t a
s
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)
-> 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
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))
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
writeDefaultSMT2 :: SMTLib2Tweaks a
=> a
-> String
-> ProblemFeatures
-> Maybe (CFG.ConfigOption I.BaseBoolType)
-> 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
startSolver
:: SMTLib2GenericSolver a
=> a
-> AcknowledgementAction t (Writer a)
-> (WriterConn t (Writer a) -> IO ())
-> SolverGoalTimeout
-> ProblemFeatures
-> Maybe (CFG.ConfigOption I.BaseBoolType)
-> 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)
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
WriterConn t (Writer a) -> IO ()
setup WriterConn t (Writer a)
writer
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
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
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)
defaultSolverBounds :: Map Text SolverBounds
defaultSolverBounds :: Map Text SolverBounds
defaultSolverBounds = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList $(computeDefaultSolverBounds)
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"
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
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
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
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
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