{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Eta reduce" #-}
module Grisette.Internal.SymPrim.TabularFun
( type (=->) (..),
)
where
import Control.DeepSeq (NFData, NFData1)
import Data.Bifunctor (Bifunctor (second))
import Data.Hashable (Hashable)
import qualified Data.SBV as SBV
import qualified Data.SBV.Dynamic as SBVD
import GHC.Generics (Generic, Generic1)
import Grisette.Internal.Core.Data.Class.Function (Function ((#)))
import Grisette.Internal.SymPrim.Prim.Internal.IsZero (KnownIsZero)
import Grisette.Internal.SymPrim.Prim.Internal.PartialEval (totalize2)
import Grisette.Internal.SymPrim.Prim.Internal.Term
( NonFuncSBVRep (NonFuncSBVBaseType),
PEvalApplyTerm (pevalApplyTerm, sbvApplyTerm),
SBVRep (SBVType),
SupportedNonFuncPrim (conNonFuncSBVTerm, withNonFuncPrim),
SupportedPrim
( conSBVTerm,
defaultValue,
parseSMTModelResult,
pevalITETerm,
sbvEq,
sbvIte,
symSBVName,
symSBVTerm,
withPrim
),
SupportedPrimConstraint (PrimConstraint),
Term (ConTerm),
applyTerm,
conTerm,
partitionCVArg,
pevalDefaultEqTerm,
pevalEqTerm,
pevalITEBasicTerm,
translateTypeError,
)
import Language.Haskell.TH.Syntax (Lift)
import Type.Reflection (typeRep)
data (=->) a b = TabularFun {forall a b. (a =-> b) -> [(a, b)]
funcTable :: [(a, b)], forall a b. (a =-> b) -> b
defaultFuncValue :: b}
deriving (Int -> (a =-> b) -> ShowS
[a =-> b] -> ShowS
(a =-> b) -> String
(Int -> (a =-> b) -> ShowS)
-> ((a =-> b) -> String) -> ([a =-> b] -> ShowS) -> Show (a =-> b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> (a =-> b) -> ShowS
forall a b. (Show a, Show b) => [a =-> b] -> ShowS
forall a b. (Show a, Show b) => (a =-> b) -> String
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> (a =-> b) -> ShowS
showsPrec :: Int -> (a =-> b) -> ShowS
$cshow :: forall a b. (Show a, Show b) => (a =-> b) -> String
show :: (a =-> b) -> String
$cshowList :: forall a b. (Show a, Show b) => [a =-> b] -> ShowS
showList :: [a =-> b] -> ShowS
Show, (a =-> b) -> (a =-> b) -> Bool
((a =-> b) -> (a =-> b) -> Bool)
-> ((a =-> b) -> (a =-> b) -> Bool) -> Eq (a =-> b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => (a =-> b) -> (a =-> b) -> Bool
$c== :: forall a b. (Eq a, Eq b) => (a =-> b) -> (a =-> b) -> Bool
== :: (a =-> b) -> (a =-> b) -> Bool
$c/= :: forall a b. (Eq a, Eq b) => (a =-> b) -> (a =-> b) -> Bool
/= :: (a =-> b) -> (a =-> b) -> Bool
Eq, (forall x. (a =-> b) -> Rep (a =-> b) x)
-> (forall x. Rep (a =-> b) x -> a =-> b) -> Generic (a =-> b)
forall x. Rep (a =-> b) x -> a =-> b
forall x. (a =-> b) -> Rep (a =-> b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a b x. Rep (a =-> b) x -> a =-> b
forall a b x. (a =-> b) -> Rep (a =-> b) x
$cfrom :: forall a b x. (a =-> b) -> Rep (a =-> b) x
from :: forall x. (a =-> b) -> Rep (a =-> b) x
$cto :: forall a b x. Rep (a =-> b) x -> a =-> b
to :: forall x. Rep (a =-> b) x -> a =-> b
Generic, (forall a. (a =-> a) -> Rep1 ((=->) a) a)
-> (forall a. Rep1 ((=->) a) a -> a =-> a) -> Generic1 ((=->) a)
forall a. Rep1 ((=->) a) a -> a =-> a
forall a. (a =-> a) -> Rep1 ((=->) a) a
forall a a. Rep1 ((=->) a) a -> a =-> a
forall a a. (a =-> a) -> Rep1 ((=->) a) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall a a. (a =-> a) -> Rep1 ((=->) a) a
from1 :: forall a. (a =-> a) -> Rep1 ((=->) a) a
$cto1 :: forall a a. Rep1 ((=->) a) a -> a =-> a
to1 :: forall a. Rep1 ((=->) a) a -> a =-> a
Generic1, (forall (m :: * -> *). Quote m => (a =-> b) -> m Exp)
-> (forall (m :: * -> *). Quote m => (a =-> b) -> Code m (a =-> b))
-> Lift (a =-> b)
forall a b (m :: * -> *).
(Lift a, Lift b, Quote m) =>
(a =-> b) -> m Exp
forall a b (m :: * -> *).
(Lift a, Lift b, Quote m) =>
(a =-> b) -> Code m (a =-> b)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => (a =-> b) -> m Exp
forall (m :: * -> *). Quote m => (a =-> b) -> Code m (a =-> b)
$clift :: forall a b (m :: * -> *).
(Lift a, Lift b, Quote m) =>
(a =-> b) -> m Exp
lift :: forall (m :: * -> *). Quote m => (a =-> b) -> m Exp
$cliftTyped :: forall a b (m :: * -> *).
(Lift a, Lift b, Quote m) =>
(a =-> b) -> Code m (a =-> b)
liftTyped :: forall (m :: * -> *). Quote m => (a =-> b) -> Code m (a =-> b)
Lift, (a =-> b) -> ()
((a =-> b) -> ()) -> NFData (a =-> b)
forall a. (a -> ()) -> NFData a
forall a b. (NFData a, NFData b) => (a =-> b) -> ()
$crnf :: forall a b. (NFData a, NFData b) => (a =-> b) -> ()
rnf :: (a =-> b) -> ()
NFData, (forall a. (a -> ()) -> (a =-> a) -> ()) -> NFData1 ((=->) a)
forall a a. NFData a => (a -> ()) -> (a =-> a) -> ()
forall a. (a -> ()) -> (a =-> a) -> ()
forall (f :: * -> *).
(forall a. (a -> ()) -> f a -> ()) -> NFData1 f
$cliftRnf :: forall a a. NFData a => (a -> ()) -> (a =-> a) -> ()
liftRnf :: forall a. (a -> ()) -> (a =-> a) -> ()
NFData1)
infixr 0 =->
instance (Eq a) => Function (a =-> b) a b where
(TabularFun [(a, b)]
table b
d) # :: (a =-> b) -> a -> b
# a
a = [(a, b)] -> b
go [(a, b)]
table
where
go :: [(a, b)] -> b
go [] = b
d
go ((a
av, b
bv) : [(a, b)]
s)
| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
av = b
bv
| Bool
otherwise = [(a, b)] -> b
go [(a, b)]
s
instance (Hashable a, Hashable b) => Hashable (a =-> b)
instance
(SupportedNonFuncPrim a, SupportedPrim b) =>
SupportedPrimConstraint (a =-> b)
where
type
PrimConstraint n (a =-> b) =
( SupportedNonFuncPrim a,
SupportedPrim b,
PrimConstraint n b
)
instance (SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a =-> b) where
type SBVType n (a =-> b) = SBV.SBV (NonFuncSBVBaseType n a) -> SBVType n b
parseTabularFunSMTModelResult ::
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int ->
([([SBVD.CV], SBVD.CV)], SBVD.CV) ->
a =-> b
parseTabularFunSMTModelResult :: forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult Int
level ([([CV], CV)]
l, CV
s) =
[(a, b)] -> b -> a =-> b
forall a b. [(a, b)] -> b -> a =-> b
TabularFun
( ([([CV], CV)] -> b) -> (a, [([CV], CV)]) -> (a, b)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second
(\[([CV], CV)]
r -> Int -> ([([CV], CV)], CV) -> b
forall t. SupportedPrim t => Int -> ([([CV], CV)], CV) -> t
parseSMTModelResult (Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ([([CV], CV)]
r, CV
s))
((a, [([CV], CV)]) -> (a, b)) -> [(a, [([CV], CV)])] -> [(a, b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
SupportedNonFuncPrim a =>
[([CV], CV)] -> [(a, [([CV], CV)])]
partitionCVArg @a [([CV], CV)]
l
)
(Int -> ([([CV], CV)], CV) -> b
forall t. SupportedPrim t => Int -> ([([CV], CV)], CV) -> t
parseSMTModelResult (Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ([], CV
s))
instance
(SupportedNonFuncPrim a, SupportedNonFuncPrim b) =>
SupportedPrim (a =-> b)
where
defaultValue :: a =-> b
defaultValue = [(a, b)] -> b -> a =-> b
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b
forall t. SupportedPrim t => t
defaultValue
pevalITETerm :: Term Bool -> Term (a =-> b) -> Term (a =-> b) -> Term (a =-> b)
pevalITETerm = Term Bool -> Term (a =-> b) -> Term (a =-> b) -> Term (a =-> b)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
pevalEqTerm :: Term (a =-> b) -> Term (a =-> b) -> Term Bool
pevalEqTerm = Term (a =-> b) -> Term (a =-> b) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> (a =-> b) -> SBVType n (a =-> b)
conSBVTerm proxy n
p a =-> b
f =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
SBVType n (a =-> b))
-> SBVType n (a =-> b))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
SBVType n (a =-> b))
-> SBVType n (a =-> b)
forall a b. (a -> b) -> a -> b
$
proxy n -> (a =-> b) -> SBV (NonFuncSBVBaseType n a) -> SBVType n b
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
Mergeable (SBVType integerBitWidth b),
KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> b
f
symSBVName :: TypedSymbol (a =-> b) -> Int -> String
symSBVName TypedSymbol (a =-> b)
_ Int
num = String
"tfunc2" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n (a =-> b))
symSBVTerm (proxy n
p :: proxy n) String
name =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType n (a =-> b)))
-> m (SBVType n (a =-> b)))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType n (a =-> b)))
-> m (SBVType n (a =-> b))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType n (a =-> b)))
-> m (SBVType n (a =-> b)))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType n (a =-> b)))
-> m (SBVType n (a =-> b))
forall a b. (a -> b) -> a -> b
$
SBVType n (a =-> b) -> m (SBVType n (a =-> b))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType n (a =-> b) -> m (SBVType n (a =-> b)))
-> SBVType n (a =-> b) -> m (SBVType n (a =-> b))
forall a b. (a -> b) -> a -> b
$
String
-> SBV (NonFuncSBVBaseType n a) -> SBV (NonFuncSBVBaseType n b)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (a =-> b),
SMTDefinable (SBVType n (a =-> b)),
Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) =>
a)
-> a
withPrim p n
p (PrimConstraint n (a =-> b), SMTDefinable (SBVType n (a =-> b)),
Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) =>
a
r = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$ forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b p n
p a
(SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a
(PrimConstraint n (a =-> b), SMTDefinable (SBVType n (a =-> b)),
Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) =>
a
r
sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (a =-> b)
-> SBVType n (a =-> b)
-> SBVType n (a =-> b)
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b proxy n
p (SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a) -> SBVType n b)
-> (SBV (NonFuncSBVBaseType n a) -> SBVType n b)
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n b
SBV Bool
-> (SBV (NonFuncSBVBaseType n a) -> SBV (NonFuncSBVBaseType n b))
-> (SBV (NonFuncSBVBaseType n a) -> SBV (NonFuncSBVBaseType n b))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a) -> SBVType n b)
-> (SBV (NonFuncSBVBaseType n a) -> SBVType n b)
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n b
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> SBVType n (a =-> b) -> SBVType n (a =-> b) -> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> b)
_ =
Maybe String
-> TypeRep (a =-> b)
-> (SBV (NonFuncSBVBaseType n a) -> SBVType n b)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
String
"BUG. Please send a bug report. TabularFun is not supported for "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
)
(forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b))
parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> b
parseSMTModelResult = Int -> ([([CV], CV)], CV) -> a =-> b
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult
instance
{-# OVERLAPPING #-}
( SupportedNonFuncPrim a,
SupportedNonFuncPrim b,
SupportedNonFuncPrim c,
SupportedPrim a,
SupportedPrim b,
SupportedPrim c
) =>
SupportedPrim (a =-> b =-> c)
where
defaultValue :: a =-> (b =-> c)
defaultValue = [(a, b =-> c)] -> (b =-> c) -> a =-> (b =-> c)
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b =-> c
forall t. SupportedPrim t => t
defaultValue
pevalITETerm :: Term Bool
-> Term (a =-> (b =-> c))
-> Term (a =-> (b =-> c))
-> Term (a =-> (b =-> c))
pevalITETerm = Term Bool
-> Term (a =-> (b =-> c))
-> Term (a =-> (b =-> c))
-> Term (a =-> (b =-> c))
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
pevalEqTerm :: Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c)) -> Term Bool
pevalEqTerm = Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c)) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c))
conSBVTerm proxy n
p a =-> (b =-> c)
f =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
SBVType n (a =-> (b =-> c)))
-> SBVType n (a =-> (b =-> c)))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
SBVType n (a =-> (b =-> c)))
-> SBVType n (a =-> (b =-> c))
forall a b. (a -> b) -> a -> b
$
proxy n
-> (a =-> (b =-> c))
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n (b =-> c)
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
Mergeable (SBVType integerBitWidth b),
KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> (b =-> c)
f
symSBVName :: TypedSymbol (a =-> (b =-> c)) -> Int -> String
symSBVName TypedSymbol (a =-> (b =-> c))
_ Int
num = String
"tfunc3" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n (a =-> (b =-> c)))
symSBVTerm (proxy n
p :: proxy n) String
name =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType n (a =-> (b =-> c))))
-> m (SBVType n (a =-> (b =-> c))))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType n (a =-> (b =-> c))))
-> m (SBVType n (a =-> (b =-> c)))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType n (a =-> (b =-> c))))
-> m (SBVType n (a =-> (b =-> c))))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType n (a =-> (b =-> c))))
-> m (SBVType n (a =-> (b =-> c)))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
m (SBVType n (a =-> (b =-> c))))
-> m (SBVType n (a =-> (b =-> c))))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
m (SBVType n (a =-> (b =-> c))))
-> m (SBVType n (a =-> (b =-> c)))
forall a b. (a -> b) -> a -> b
$
SBVType n (a =-> (b =-> c)) -> m (SBVType n (a =-> (b =-> c)))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType n (a =-> (b =-> c)) -> m (SBVType n (a =-> (b =-> c))))
-> SBVType n (a =-> (b =-> c)) -> m (SBVType n (a =-> (b =-> c)))
forall a b. (a -> b) -> a -> b
$
String
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (a =-> (b =-> c)),
SMTDefinable (SBVType n (a =-> (b =-> c))),
Mergeable (SBVType n (a =-> (b =-> c))),
Typeable (SBVType n (a =-> (b =-> c)))) =>
a)
-> a
withPrim p n
p (PrimConstraint n (a =-> (b =-> c)),
SMTDefinable (SBVType n (a =-> (b =-> c))),
Mergeable (SBVType n (a =-> (b =-> c))),
Typeable (SBVType n (a =-> (b =-> c)))) =>
a
r =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b p n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c p n
p a
(SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
a
(PrimConstraint n (a =-> (b =-> c)),
SMTDefinable (SBVType n (a =-> (b =-> c))),
Mergeable (SBVType n (a =-> (b =-> c))),
Typeable (SBVType n (a =-> (b =-> c)))) =>
a
r
sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (a =-> (b =-> c))
-> SBVType n (a =-> (b =-> c))
-> SBVType n (a =-> (b =-> c))
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c proxy n
p (SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b) -> SBVType n c)
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b) -> SBVType n c)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBVType n c
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b) -> SBV (NonFuncSBVBaseType n c))
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b) -> SBV (NonFuncSBVBaseType n c))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b) -> SBVType n c)
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b) -> SBVType n c)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBVType n c
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType n (a =-> (b =-> c))
-> SBVType n (a =-> (b =-> c))
-> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> (b =-> c))
_ =
Maybe String
-> TypeRep (a =-> (b =-> c))
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b) -> SBVType n c)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
String
"BUG. Please send a bug report. TabularFun is not supported for "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
)
(forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b =-> c))
parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> c)
parseSMTModelResult = Int -> ([([CV], CV)], CV) -> a =-> (b =-> c)
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult
instance
{-# OVERLAPPING #-}
( SupportedNonFuncPrim a,
SupportedNonFuncPrim b,
SupportedNonFuncPrim c,
SupportedNonFuncPrim d,
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d
) =>
SupportedPrim (a =-> b =-> c =-> d)
where
defaultValue :: a =-> (b =-> (c =-> d))
defaultValue = [(a, b =-> (c =-> d))]
-> (b =-> (c =-> d)) -> a =-> (b =-> (c =-> d))
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b =-> (c =-> d)
forall t. SupportedPrim t => t
defaultValue
pevalITETerm :: Term Bool
-> Term (a =-> (b =-> (c =-> d)))
-> Term (a =-> (b =-> (c =-> d)))
-> Term (a =-> (b =-> (c =-> d)))
pevalITETerm = Term Bool
-> Term (a =-> (b =-> (c =-> d)))
-> Term (a =-> (b =-> (c =-> d)))
-> Term (a =-> (b =-> (c =-> d)))
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
pevalEqTerm :: Term (a =-> (b =-> (c =-> d)))
-> Term (a =-> (b =-> (c =-> d))) -> Term Bool
pevalEqTerm = Term (a =-> (b =-> (c =-> d)))
-> Term (a =-> (b =-> (c =-> d))) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d)))
conSBVTerm proxy n
p a =-> (b =-> (c =-> d))
f =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @d proxy n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
SBVType n (a =-> (b =-> (c =-> d))))
-> SBVType n (a =-> (b =-> (c =-> d))))
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
SBVType n (a =-> (b =-> (c =-> d))))
-> SBVType n (a =-> (b =-> (c =-> d)))
forall a b. (a -> b) -> a -> b
$
proxy n
-> (a =-> (b =-> (c =-> d)))
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n (b =-> (c =-> d))
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
Mergeable (SBVType integerBitWidth b),
KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> (b =-> (c =-> d))
f
symSBVName :: TypedSymbol (a =-> (b =-> (c =-> d))) -> Int -> String
symSBVName TypedSymbol (a =-> (b =-> (c =-> d)))
_ Int
num = String
"tfunc4" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> d))))
symSBVTerm (proxy n
p :: proxy n) String
name =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType n (a =-> (b =-> (c =-> d)))))
-> m (SBVType n (a =-> (b =-> (c =-> d)))))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType n (a =-> (b =-> (c =-> d)))))
-> m (SBVType n (a =-> (b =-> (c =-> d))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType n (a =-> (b =-> (c =-> d)))))
-> m (SBVType n (a =-> (b =-> (c =-> d)))))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType n (a =-> (b =-> (c =-> d)))))
-> m (SBVType n (a =-> (b =-> (c =-> d))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
m (SBVType n (a =-> (b =-> (c =-> d)))))
-> m (SBVType n (a =-> (b =-> (c =-> d)))))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
m (SBVType n (a =-> (b =-> (c =-> d)))))
-> m (SBVType n (a =-> (b =-> (c =-> d))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @d proxy n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
m (SBVType n (a =-> (b =-> (c =-> d)))))
-> m (SBVType n (a =-> (b =-> (c =-> d)))))
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
m (SBVType n (a =-> (b =-> (c =-> d)))))
-> m (SBVType n (a =-> (b =-> (c =-> d))))
forall a b. (a -> b) -> a -> b
$
SBVType n (a =-> (b =-> (c =-> d)))
-> m (SBVType n (a =-> (b =-> (c =-> d))))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType n (a =-> (b =-> (c =-> d)))
-> m (SBVType n (a =-> (b =-> (c =-> d)))))
-> SBVType n (a =-> (b =-> (c =-> d)))
-> m (SBVType n (a =-> (b =-> (c =-> d))))
forall a b. (a -> b) -> a -> b
$
String
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (a =-> (b =-> (c =-> d))),
SMTDefinable (SBVType n (a =-> (b =-> (c =-> d)))),
Mergeable (SBVType n (a =-> (b =-> (c =-> d)))),
Typeable (SBVType n (a =-> (b =-> (c =-> d))))) =>
a)
-> a
withPrim p n
p (PrimConstraint n (a =-> (b =-> (c =-> d))),
SMTDefinable (SBVType n (a =-> (b =-> (c =-> d)))),
Mergeable (SBVType n (a =-> (b =-> (c =-> d)))),
Typeable (SBVType n (a =-> (b =-> (c =-> d))))) =>
a
r =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b p n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c p n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @d p n
p a
(SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
a
(PrimConstraint n (a =-> (b =-> (c =-> d))),
SMTDefinable (SBVType n (a =-> (b =-> (c =-> d)))),
Mergeable (SBVType n (a =-> (b =-> (c =-> d)))),
Typeable (SBVType n (a =-> (b =-> (c =-> d))))) =>
a
r
sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (a =-> (b =-> (c =-> d)))
-> SBVType n (a =-> (b =-> (c =-> d)))
-> SBVType n (a =-> (b =-> (c =-> d)))
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @d proxy n
p (SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBVType n d)
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBVType n d)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBVType n d
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d))
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBVType n d)
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBVType n d)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBVType n d
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType n (a =-> (b =-> (c =-> d)))
-> SBVType n (a =-> (b =-> (c =-> d)))
-> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> (b =-> (c =-> d)))
_ =
Maybe String
-> TypeRep (a =-> (b =-> (c =-> d)))
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBVType n d)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
String
"BUG. Please send a bug report. TabularFun is not supported for "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
)
(forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b =-> c =-> d))
parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> d))
parseSMTModelResult = Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> d))
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult
instance
{-# OVERLAPPING #-}
( SupportedNonFuncPrim a,
SupportedNonFuncPrim b,
SupportedNonFuncPrim c,
SupportedNonFuncPrim d,
SupportedNonFuncPrim e,
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d,
SupportedPrim e
) =>
SupportedPrim (a =-> b =-> c =-> d =-> e)
where
defaultValue :: a =-> (b =-> (c =-> (d =-> e)))
defaultValue = [(a, b =-> (c =-> (d =-> e)))]
-> (b =-> (c =-> (d =-> e))) -> a =-> (b =-> (c =-> (d =-> e)))
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b =-> (c =-> (d =-> e))
forall t. SupportedPrim t => t
defaultValue
pevalITETerm :: Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> e))))
-> Term (a =-> (b =-> (c =-> (d =-> e))))
-> Term (a =-> (b =-> (c =-> (d =-> e))))
pevalITETerm = Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> e))))
-> Term (a =-> (b =-> (c =-> (d =-> e))))
-> Term (a =-> (b =-> (c =-> (d =-> e))))
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> e))))
-> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term Bool
pevalEqTerm = Term (a =-> (b =-> (c =-> (d =-> e))))
-> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> (a =-> (b =-> (c =-> (d =-> e))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
conSBVTerm proxy n
p a =-> (b =-> (c =-> (d =-> e)))
f =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @e proxy n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
forall a b. (a -> b) -> a -> b
$
proxy n
-> (a =-> (b =-> (c =-> (d =-> e))))
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n (b =-> (c =-> (d =-> e)))
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
Mergeable (SBVType integerBitWidth b),
KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> (b =-> (c =-> (d =-> e)))
f
symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> e)))) -> Int -> String
symSBVName TypedSymbol (a =-> (b =-> (c =-> (d =-> e))))
_ Int
num = String
"tfunc5" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n
-> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
symSBVTerm (proxy n
p :: proxy n) String
name =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @d proxy n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @e proxy n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a b. (a -> b) -> a -> b
$
SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))
forall a b. (a -> b) -> a -> b
$
String
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> e)))),
SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))),
Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))),
Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))) =>
a)
-> a
withPrim p n
p (PrimConstraint n (a =-> (b =-> (c =-> (d =-> e)))),
SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))),
Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))),
Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))) =>
a
r =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b p n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c p n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @d p n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @e p n
p a
(SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
a
(PrimConstraint n (a =-> (b =-> (c =-> (d =-> e)))),
SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))),
Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))),
Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))) =>
a
r
sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @e proxy n
p (SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBVType n e)
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBVType n e)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBVType n e
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e))
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBVType n e)
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBVType n e)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBVType n e
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> e))))
-> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> (b =-> (c =-> (d =-> e))))
_ =
Maybe String
-> TypeRep (a =-> (b =-> (c =-> (d =-> e))))
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBVType n e)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
String
"BUG. Please send a bug report. TabularFun is not supported for "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
)
(forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b =-> c =-> d =-> e))
parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> e)))
parseSMTModelResult = Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> e)))
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult
instance
{-# OVERLAPPING #-}
( SupportedNonFuncPrim a,
SupportedNonFuncPrim b,
SupportedNonFuncPrim c,
SupportedNonFuncPrim d,
SupportedNonFuncPrim e,
SupportedNonFuncPrim f,
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d,
SupportedPrim e,
SupportedPrim f
) =>
SupportedPrim (a =-> b =-> c =-> d =-> e =-> f)
where
defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> f))))
defaultValue = [(a, b =-> (c =-> (d =-> (e =-> f))))]
-> (b =-> (c =-> (d =-> (e =-> f))))
-> a =-> (b =-> (c =-> (d =-> (e =-> f))))
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b =-> (c =-> (d =-> (e =-> f)))
forall t. SupportedPrim t => t
defaultValue
pevalITETerm :: Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
pevalITETerm = Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term Bool
pevalEqTerm = Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
conSBVTerm proxy n
p a =-> (b =-> (c =-> (d =-> (e =-> f))))
f =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @f proxy n
p (((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
-> ((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
forall a b. (a -> b) -> a -> b
$
proxy n
-> (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n (b =-> (c =-> (d =-> (e =-> f))))
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
Mergeable (SBVType integerBitWidth b),
KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> (b =-> (c =-> (d =-> (e =-> f))))
f
symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> Int -> String
symSBVName TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
_ Int
num = String
"tfunc6" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n
-> String
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
symSBVTerm (proxy n
p :: proxy n) String
name =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @d proxy n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @e proxy n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @f proxy n
p (((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> ((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))
forall a b. (a -> b) -> a -> b
$
String
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> f))))),
SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))),
Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))),
Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))) =>
a)
-> a
withPrim p n
p (PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> f))))),
SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))),
Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))),
Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))) =>
a
r =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b p n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c p n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @d p n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @e p n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @f p n
p a
(SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
a
(PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> f))))),
SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))),
Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))),
Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))) =>
a
r
sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @f proxy n
p (SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBVType n f)
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBVType n f)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBVType n f
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f))
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBVType n f)
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBVType n f)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBVType n f
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
_ =
Maybe String
-> TypeRep (a =-> (b =-> (c =-> (d =-> (e =-> f)))))
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBVType n f)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
String
"BUG. Please send a bug report. TabularFun is not supported for "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
)
(forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b =-> c =-> d =-> e =-> f))
parseSMTModelResult :: Int
-> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> f))))
parseSMTModelResult = Int
-> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> f))))
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult
instance
{-# OVERLAPPING #-}
( SupportedNonFuncPrim a,
SupportedNonFuncPrim b,
SupportedNonFuncPrim c,
SupportedNonFuncPrim d,
SupportedNonFuncPrim e,
SupportedNonFuncPrim f,
SupportedNonFuncPrim g,
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d,
SupportedPrim e,
SupportedPrim f,
SupportedPrim g
) =>
SupportedPrim (a =-> b =-> c =-> d =-> e =-> f =-> g)
where
defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
defaultValue = [(a, b =-> (c =-> (d =-> (e =-> (f =-> g)))))]
-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
-> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b =-> (c =-> (d =-> (e =-> (f =-> g))))
forall t. SupportedPrim t => t
defaultValue
pevalITETerm :: Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
pevalITETerm = Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term Bool
pevalEqTerm = Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
conSBVTerm proxy n
p a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
f =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @g proxy n
p (((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
Mergeable (SBVType n g), SMTDefinable (SBVType n g),
Mergeable (SBVType n g),
SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
-> ((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
Mergeable (SBVType n g), SMTDefinable (SBVType n g),
Mergeable (SBVType n g),
SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
forall a b. (a -> b) -> a -> b
$
proxy n
-> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
Mergeable (SBVType integerBitWidth b),
KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
f
symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> Int -> String
symSBVName TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
_ Int
num = String
"tfunc7" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n
-> String
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
symSBVTerm (proxy n
p :: proxy n) String
name =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @d proxy n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @e proxy n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @f proxy n
p (((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @g proxy n
p (((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
Mergeable (SBVType n g), SMTDefinable (SBVType n g),
Mergeable (SBVType n g),
SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> ((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
Mergeable (SBVType n g), SMTDefinable (SBVType n g),
Mergeable (SBVType n g),
SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))
forall a b. (a -> b) -> a -> b
$
String
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))),
SMTDefinable
(SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))),
Mergeable
(SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))),
Typeable
(SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))) =>
a)
-> a
withPrim p n
p (PrimConstraint
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))),
SMTDefinable
(SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))),
Mergeable
(SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))),
Typeable
(SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))) =>
a
r =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b p n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c p n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @d p n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @e p n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @f p n
p (((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @g p n
p a
(SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
Mergeable (SBVType n g), SMTDefinable (SBVType n g),
Mergeable (SBVType n g),
SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
a
(PrimConstraint
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))),
SMTDefinable
(SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))),
Mergeable
(SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))),
Typeable
(SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))) =>
a
r
sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @g proxy n
p (SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
Mergeable (SBVType n g), SMTDefinable (SBVType n g),
Mergeable (SBVType n g),
SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBVType n g)
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBVType n g)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBVType n g
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g))
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBVType n g)
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBVType n g)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBVType n g
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
_ =
Maybe String
-> TypeRep (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBVType n g)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
String
"BUG. Please send a bug report. TabularFun is not supported for "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
)
(forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b =-> c =-> d =-> e =-> f =-> g))
parseSMTModelResult :: Int
-> ([([CV], CV)], CV)
-> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
parseSMTModelResult = Int
-> ([([CV], CV)], CV)
-> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult
instance
{-# OVERLAPPING #-}
( SupportedNonFuncPrim a,
SupportedNonFuncPrim b,
SupportedNonFuncPrim c,
SupportedNonFuncPrim d,
SupportedNonFuncPrim e,
SupportedNonFuncPrim f,
SupportedNonFuncPrim g,
SupportedNonFuncPrim h,
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d,
SupportedPrim e,
SupportedPrim f,
SupportedPrim g,
SupportedPrim h
) =>
SupportedPrim (a =-> b =-> c =-> d =-> e =-> f =-> g =-> h)
where
defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
defaultValue = [(a, b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))]
-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
-> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))
forall t. SupportedPrim t => t
defaultValue
pevalITETerm :: Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
pevalITETerm = Term Bool
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term Bool
pevalEqTerm = Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
conSBVTerm proxy n
p a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
f =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @h proxy n
p (((SymVal (NonFuncSBVBaseType n h), EqSymbolic (SBVType n h),
Mergeable (SBVType n h), SMTDefinable (SBVType n h),
Mergeable (SBVType n h),
SBVType n h ~ SBV (NonFuncSBVBaseType n h), PrimConstraint n h) =>
SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
-> SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
-> ((SymVal (NonFuncSBVBaseType n h), EqSymbolic (SBVType n h),
Mergeable (SBVType n h), SMTDefinable (SBVType n h),
Mergeable (SBVType n h),
SBVType n h ~ SBV (NonFuncSBVBaseType n h), PrimConstraint n h) =>
SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
-> SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
forall a b. (a -> b) -> a -> b
$
proxy n
-> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> SBV (NonFuncSBVBaseType n a)
-> SBVType n (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
Mergeable (SBVType integerBitWidth b),
KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy n
p a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
f
symSBVName :: TypedSymbol
(a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> Int -> String
symSBVName TypedSymbol
(a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
_ Int
num = String
"tfunc8" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
num
symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n
-> String
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
symSBVTerm (proxy n
p :: proxy n) String
name =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b proxy n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c proxy n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @d proxy n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @e proxy n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @f proxy n
p (((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @g proxy n
p (((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
Mergeable (SBVType n g), SMTDefinable (SBVType n g),
Mergeable (SBVType n g),
SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
Mergeable (SBVType n g), SMTDefinable (SBVType n g),
Mergeable (SBVType n g),
SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @h proxy n
p (((SymVal (NonFuncSBVBaseType n h), EqSymbolic (SBVType n h),
Mergeable (SBVType n h), SMTDefinable (SBVType n h),
Mergeable (SBVType n h),
SBVType n h ~ SBV (NonFuncSBVBaseType n h), PrimConstraint n h) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> ((SymVal (NonFuncSBVBaseType n h), EqSymbolic (SBVType n h),
Mergeable (SBVType n h), SMTDefinable (SBVType n h),
Mergeable (SBVType n h),
SBVType n h ~ SBV (NonFuncSBVBaseType n h), PrimConstraint n h) =>
m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))))
-> SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> m (SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))
forall a b. (a -> b) -> a -> b
$
String
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBV (NonFuncSBVBaseType n h)
forall a. SMTDefinable a => String -> a
SBV.uninterpret String
name
withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))),
SMTDefinable
(SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))),
Mergeable
(SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))),
Typeable
(SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))) =>
a)
-> a
withPrim p n
p (PrimConstraint
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))),
SMTDefinable
(SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))),
Mergeable
(SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))),
Typeable
(SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))) =>
a
r =
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a p n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @b p n
p (((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n b), EqSymbolic (SBVType n b),
Mergeable (SBVType n b), SMTDefinable (SBVType n b),
Mergeable (SBVType n b),
SBVType n b ~ SBV (NonFuncSBVBaseType n b), PrimConstraint n b) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @c p n
p (((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n c), EqSymbolic (SBVType n c),
Mergeable (SBVType n c), SMTDefinable (SBVType n c),
Mergeable (SBVType n c),
SBVType n c ~ SBV (NonFuncSBVBaseType n c), PrimConstraint n c) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @d p n
p (((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n d), EqSymbolic (SBVType n d),
Mergeable (SBVType n d), SMTDefinable (SBVType n d),
Mergeable (SBVType n d),
SBVType n d ~ SBV (NonFuncSBVBaseType n d), PrimConstraint n d) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @e p n
p (((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n e), EqSymbolic (SBVType n e),
Mergeable (SBVType n e), SMTDefinable (SBVType n e),
Mergeable (SBVType n e),
SBVType n e ~ SBV (NonFuncSBVBaseType n e), PrimConstraint n e) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @f p n
p (((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n f), EqSymbolic (SBVType n f),
Mergeable (SBVType n f), SMTDefinable (SBVType n f),
Mergeable (SBVType n f),
SBVType n f ~ SBV (NonFuncSBVBaseType n f), PrimConstraint n f) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @g p n
p (((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
Mergeable (SBVType n g), SMTDefinable (SBVType n g),
Mergeable (SBVType n g),
SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
a)
-> a)
-> ((SymVal (NonFuncSBVBaseType n g), EqSymbolic (SBVType n g),
Mergeable (SBVType n g), SMTDefinable (SBVType n g),
Mergeable (SBVType n g),
SBVType n g ~ SBV (NonFuncSBVBaseType n g), PrimConstraint n g) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @h p n
p a
(SymVal (NonFuncSBVBaseType n h), EqSymbolic (SBVType n h),
Mergeable (SBVType n h), SMTDefinable (SBVType n h),
Mergeable (SBVType n h),
SBVType n h ~ SBV (NonFuncSBVBaseType n h), PrimConstraint n h) =>
a
(PrimConstraint
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))),
SMTDefinable
(SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))),
Mergeable
(SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))),
Typeable
(SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))) =>
a
r
sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
sbvIte proxy n
p = forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @h proxy n
p (SymVal (NonFuncSBVBaseType n h), EqSymbolic (SBVType n h),
Mergeable (SBVType n h), SMTDefinable (SBVType n h),
Mergeable (SBVType n h),
SBVType n h ~ SBV (NonFuncSBVBaseType n h), PrimConstraint n h) =>
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBVType n h)
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBVType n h)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBVType n h
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBV (NonFuncSBVBaseType n h))
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBV (NonFuncSBVBaseType n h))
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBV (NonFuncSBVBaseType n h)
SBV Bool
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBVType n h)
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBVType n h)
-> SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBVType n h
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
sbvEq :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> SBVType
n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> SBV Bool
sbvEq proxy n
_ SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
_ =
Maybe String
-> TypeRep
(a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))
-> (SBV (NonFuncSBVBaseType n a)
-> SBV (NonFuncSBVBaseType n b)
-> SBV (NonFuncSBVBaseType n c)
-> SBV (NonFuncSBVBaseType n d)
-> SBV (NonFuncSBVBaseType n e)
-> SBV (NonFuncSBVBaseType n f)
-> SBV (NonFuncSBVBaseType n g)
-> SBVType n h)
-> SBV Bool
forall a b. HasCallStack => Maybe String -> TypeRep a -> b
translateTypeError
( String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
String
"BUG. Please send a bug report. TabularFun is not supported for "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"equality comparison."
)
(forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(a =-> b =-> c =-> d =-> e =-> f =-> g =-> h))
parseSMTModelResult :: Int
-> ([([CV], CV)], CV)
-> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
parseSMTModelResult = Int
-> ([([CV], CV)], CV)
-> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a =-> b
parseTabularFunSMTModelResult
instance
(SupportedPrim a, SupportedPrim b, SupportedPrim (a =-> b)) =>
PEvalApplyTerm (a =-> b) a b
where
pevalApplyTerm :: Term (a =-> b) -> Term a -> Term b
pevalApplyTerm = (Term (a =-> b) -> PartialFun (Term a) (Term b))
-> (Term (a =-> b) -> Term a -> Term b)
-> Term (a =-> b)
-> Term a
-> Term b
forall a b c. (a -> PartialFun b c) -> (a -> b -> c) -> a -> b -> c
totalize2 Term (a =-> b) -> PartialFun (Term a) (Term b)
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> PartialFun (Term a) (Term b)
doPevalApplyTerm Term (a =-> b) -> Term a -> Term b
forall a b f.
(SupportedPrim a, SupportedPrim b, SupportedPrim f,
PEvalApplyTerm f a b) =>
Term f -> Term a -> Term b
applyTerm
where
doPevalApplyTerm ::
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) ->
Term a ->
Maybe (Term b)
doPevalApplyTerm :: (SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> PartialFun (Term a) (Term b)
doPevalApplyTerm (ConTerm Int
_ a =-> b
f) (ConTerm Int
_ a
a) = Term b -> Maybe (Term b)
forall a. a -> Maybe a
Just (Term b -> Maybe (Term b)) -> Term b -> Maybe (Term b)
forall a b. (a -> b) -> a -> b
$ b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (b -> Term b) -> b -> Term b
forall a b. (a -> b) -> a -> b
$ a =-> b
f (a =-> b) -> a -> b
forall f arg ret. Function f arg ret => f -> arg -> ret
# a
a
doPevalApplyTerm (ConTerm Int
_ (TabularFun [(a, b)]
f b
d)) Term a
a = Term b -> Maybe (Term b)
forall a. a -> Maybe a
Just (Term b -> Maybe (Term b)) -> Term b -> Maybe (Term b)
forall a b. (a -> b) -> a -> b
$ [(a, b)] -> Term b
go [(a, b)]
f
where
go :: [(a, b)] -> Term b
go [] = b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm b
d
go ((a
x, b
y) : [(a, b)]
xs) =
Term Bool -> Term b -> Term b -> Term b
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm (Term a -> Term a -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqTerm Term a
a (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
x)) (b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm b
y) ([(a, b)] -> Term b
go [(a, b)]
xs)
doPevalApplyTerm Term (a =-> b)
_ Term a
_ = Maybe (Term b)
forall a. Maybe a
Nothing
sbvApplyTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> SBVType n (a =-> b) -> SBVType n a -> SBVType n b
sbvApplyTerm proxy n
p SBVType n (a =-> b)
f SBVType n a
a =
forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
Mergeable (SBVType n t), Typeable (SBVType n t)) =>
a)
-> a
withPrim @(a =-> b) proxy n
p (((PrimConstraint n (a =-> b), SMTDefinable (SBVType n (a =-> b)),
Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) =>
SBVType n b)
-> SBVType n b)
-> ((PrimConstraint n (a =-> b),
SMTDefinable (SBVType n (a =-> b)),
Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) =>
SBVType n b)
-> SBVType n b
forall a b. (a -> b) -> a -> b
$ forall a (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
r)
-> r
withNonFuncPrim @a proxy n
p (((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
SBVType n b)
-> SBVType n b)
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
Mergeable (SBVType n a), SMTDefinable (SBVType n a),
Mergeable (SBVType n a),
SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
SBVType n b)
-> SBVType n b
forall a b. (a -> b) -> a -> b
$ SBVType n (a =-> b)
SBV (NonFuncSBVBaseType n a) -> SBVType n b
f SBV (NonFuncSBVBaseType n a)
SBVType n a
a
lowerTFunCon ::
forall proxy integerBitWidth a b.
( SupportedNonFuncPrim a,
SupportedPrim b,
SBV.Mergeable (SBVType integerBitWidth b),
KnownIsZero integerBitWidth
) =>
proxy integerBitWidth ->
(a =-> b) ->
( SBV.SBV (NonFuncSBVBaseType integerBitWidth a) ->
SBVType integerBitWidth b
)
lowerTFunCon :: forall (proxy :: Nat -> *) (integerBitWidth :: Nat) a b.
(SupportedNonFuncPrim a, SupportedPrim b,
Mergeable (SBVType integerBitWidth b),
KnownIsZero integerBitWidth) =>
proxy integerBitWidth
-> (a =-> b)
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
lowerTFunCon proxy integerBitWidth
proxy (TabularFun [(a, b)]
l b
d) = [(a, b)]
-> b
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
go [(a, b)]
l b
d
where
go :: [(a, b)]
-> b
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
go [] b
d SBV (NonFuncSBVBaseType integerBitWidth a)
_ = proxy integerBitWidth -> b -> SBVType integerBitWidth b
forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> b -> SBVType n b
forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm proxy integerBitWidth
proxy b
d
go ((a
x, b
r) : [(a, b)]
xs) b
d SBV (NonFuncSBVBaseType integerBitWidth a)
v =
SBV Bool
-> SBVType integerBitWidth b
-> SBVType integerBitWidth b
-> SBVType integerBitWidth b
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite
(proxy integerBitWidth
-> a -> SBV (NonFuncSBVBaseType integerBitWidth a)
forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> a -> SBV (NonFuncSBVBaseType n a)
forall a (n :: Nat) (proxy :: Nat -> *).
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n -> a -> SBV (NonFuncSBVBaseType n a)
conNonFuncSBVTerm proxy integerBitWidth
proxy a
x SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBV (NonFuncSBVBaseType integerBitWidth a) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
SBV..== SBV (NonFuncSBVBaseType integerBitWidth a)
v)
(proxy integerBitWidth -> b -> SBVType integerBitWidth b
forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> b -> SBVType n b
forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm proxy integerBitWidth
proxy b
r)
([(a, b)]
-> b
-> SBV (NonFuncSBVBaseType integerBitWidth a)
-> SBVType integerBitWidth b
go [(a, b)]
xs b
d SBV (NonFuncSBVBaseType integerBitWidth a)
v)