{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim
  ( bvIsNonZeroFromGEq1,
  )
where

import Data.Coerce (coerce)
import Data.List.NonEmpty (NonEmpty ((:|)), toList)
import Data.Proxy (Proxy (Proxy))
import Data.SBV (BVIsNonZero)
import qualified Data.SBV as SBV
import Data.Type.Equality ((:~:) (Refl), type (:~~:) (HRefl))
import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.SymPrim.AlgReal (AlgReal, fromSBVAlgReal, toSBVAlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP
  ( FP (FP),
    FPRoundingMode (RNA, RNE, RTN, RTP, RTZ),
    ValidFP,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( IsSymbolKind (decideSymbolKind),
    NonFuncSBVRep (NonFuncSBVBaseType),
    SBVRep
      ( SBVType
      ),
    SupportedNonFuncPrim
      ( conNonFuncSBVTerm,
        symNonFuncSBVTerm,
        withNonFuncPrim
      ),
    SupportedPrim
      ( castTypedSymbol,
        conSBVTerm,
        defaultValue,
        defaultValueDynamic,
        funcDummyConstraint,
        isFuncType,
        parseSMTModelResult,
        pevalDistinctTerm,
        pevalEqTerm,
        pevalITETerm,
        pformatCon,
        sbvIte,
        symSBVName,
        symSBVTerm,
        withPrim
      ),
    SupportedPrimConstraint
      ( PrimConstraint
      ),
    Term (ConTerm),
    TypedSymbol (TypedSymbol),
    conTerm,
    distinctTerm,
    eqTerm,
    parseScalarSMTModelResult,
    pevalDefaultEqTerm,
    pevalITEBasicTerm,
    pevalNotTerm,
    sbvFresh,
  )
import Grisette.Internal.SymPrim.Prim.ModelValue (ModelValue, toModelValue)
import Grisette.Internal.Utils.Parameterized (unsafeAxiom)

defaultValueForInteger :: Integer
defaultValueForInteger :: Integer
defaultValueForInteger = Integer
0

defaultValueForIntegerDyn :: ModelValue
defaultValueForIntegerDyn :: ModelValue
defaultValueForIntegerDyn = Integer -> ModelValue
forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue Integer
defaultValueForInteger

-- Basic Integer
instance SBVRep Integer where
  type SBVType Integer = SBV.SBV Integer

instance SupportedPrimConstraint Integer where
  type PrimConstraint Integer = (Integral (NonFuncSBVBaseType Integer))

pairwiseHasConcreteEqual :: (SupportedNonFuncPrim a) => [Term a] -> Bool
pairwiseHasConcreteEqual :: forall a. SupportedNonFuncPrim a => [Term a] -> Bool
pairwiseHasConcreteEqual [] = Bool
False
pairwiseHasConcreteEqual [Term a
_] = Bool
False
pairwiseHasConcreteEqual (Term a
x : [Term a]
xs) =
  Term a -> [Term a] -> Bool
forall {t}. Eq t => t -> [t] -> Bool
go Term a
x [Term a]
xs Bool -> Bool -> Bool
|| [Term a] -> Bool
forall a. SupportedNonFuncPrim a => [Term a] -> Bool
pairwiseHasConcreteEqual [Term a]
xs
  where
    go :: t -> [t] -> Bool
go t
_ [] = Bool
False
    go t
x (t
y : [t]
ys) = t
x t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
y Bool -> Bool -> Bool
|| t -> [t] -> Bool
go t
x [t]
ys

pevalGeneralDistinct ::
  (SupportedNonFuncPrim a) => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct :: forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct (Term a
_ :| []) = Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm Bool
True
pevalGeneralDistinct (Term a
a :| [Term a
b]) = Term Bool -> Term Bool
pevalNotTerm (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term a
a Term a
b
pevalGeneralDistinct NonEmpty (Term a)
l | [Term a] -> Bool
forall a. SupportedNonFuncPrim a => [Term a] -> Bool
pairwiseHasConcreteEqual ([Term a] -> Bool) -> [Term a] -> Bool
forall a b. (a -> b) -> a -> b
$ NonEmpty (Term a) -> [Term a]
forall a. NonEmpty a -> [a]
toList NonEmpty (Term a)
l = Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm Bool
False
pevalGeneralDistinct NonEmpty (Term a)
l = NonEmpty (Term a) -> Term Bool
forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
distinctTerm NonEmpty (Term a)
l

instance SupportedPrim Integer where
  pformatCon :: Integer -> String
pformatCon = Integer -> String
forall a. Show a => a -> String
show
  defaultValue :: Integer
defaultValue = Integer
defaultValueForInteger
  defaultValueDynamic :: forall (proxy :: * -> *). proxy Integer -> ModelValue
defaultValueDynamic proxy Integer
_ = ModelValue
defaultValueForIntegerDyn
  pevalITETerm :: Term Bool -> Term Integer -> Term Integer -> Term Integer
pevalITETerm = Term Bool -> Term Integer -> Term Integer -> Term Integer
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term Integer -> Term Integer -> Term Bool
pevalEqTerm = Term Integer -> Term Integer -> Term Bool
forall a. SupportedNonFuncPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  pevalDistinctTerm :: NonEmpty (Term Integer) -> Term Bool
pevalDistinctTerm = NonEmpty (Term Integer) -> Term Bool
forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct
  conSBVTerm :: Integer -> SBVType Integer
conSBVTerm Integer
n = Integer -> SBV Integer
forall a. Num a => Integer -> a
fromInteger Integer
n
  symSBVName :: TypedSymbol 'AnyKind Integer -> Int -> String
symSBVName TypedSymbol 'AnyKind Integer
symbol Int
_ = TypedSymbol 'AnyKind Integer -> String
forall a. Show a => a -> String
show TypedSymbol 'AnyKind Integer
symbol
  symSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBVType Integer)
symSBVTerm String
name = String -> m (SBV Integer)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
  withPrim :: forall a.
((PrimConstraint Integer, SMTDefinable (SBVType Integer),
  Mergeable (SBVType Integer), Typeable (SBVType Integer)) =>
 a)
-> a
withPrim (PrimConstraint Integer, SMTDefinable (SBVType Integer),
 Mergeable (SBVType Integer), Typeable (SBVType Integer)) =>
a
r = a
(PrimConstraint Integer, SMTDefinable (SBVType Integer),
 Mergeable (SBVType Integer), Typeable (SBVType Integer)) =>
a
r
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> Integer
parseSMTModelResult Int
_ = (Integer -> Integer) -> ([([CV], CV)], CV) -> Integer
forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult Integer -> Integer
forall a. a -> a
id
  castTypedSymbol ::
    forall knd knd'.
    (IsSymbolKind knd') =>
    TypedSymbol knd Integer ->
    Maybe (TypedSymbol knd' Integer)
  castTypedSymbol :: forall (knd :: SymbolKind) (knd' :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd Integer -> Maybe (TypedSymbol knd' Integer)
castTypedSymbol (TypedSymbol Symbol
s) =
    case forall (ty :: SymbolKind).
IsSymbolKind ty =>
Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind)
decideSymbolKind @knd' of
      Left knd' :~~: 'ConstantKind
HRefl -> TypedSymbol knd' Integer -> Maybe (TypedSymbol knd' Integer)
forall a. a -> Maybe a
Just (TypedSymbol knd' Integer -> Maybe (TypedSymbol knd' Integer))
-> TypedSymbol knd' Integer -> Maybe (TypedSymbol knd' Integer)
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol knd' Integer
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
s
      Right knd' :~~: 'AnyKind
HRefl -> TypedSymbol knd' Integer -> Maybe (TypedSymbol knd' Integer)
forall a. a -> Maybe a
Just (TypedSymbol knd' Integer -> Maybe (TypedSymbol knd' Integer))
-> TypedSymbol knd' Integer -> Maybe (TypedSymbol knd' Integer)
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol knd' Integer
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
s
  isFuncType :: Bool
isFuncType = Bool
False
  funcDummyConstraint :: SBVType Integer -> SBV Bool
funcDummyConstraint SBVType Integer
_ = SBV Bool
SBV.sTrue

instance NonFuncSBVRep Integer where
  type NonFuncSBVBaseType Integer = Integer

instance SupportedNonFuncPrim Integer where
  conNonFuncSBVTerm :: Integer -> SBV (NonFuncSBVBaseType Integer)
conNonFuncSBVTerm = Integer -> SBV (NonFuncSBVBaseType Integer)
Integer -> SBVType Integer
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBV (NonFuncSBVBaseType Integer))
symNonFuncSBVTerm = forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
String -> m (SBVType t)
symSBVTerm @Integer
  withNonFuncPrim :: forall r. (NonFuncPrimConstraint Integer => r) -> r
withNonFuncPrim NonFuncPrimConstraint Integer => r
r = r
NonFuncPrimConstraint Integer => r
r

-- Signed BV
instance (KnownNat w, 1 <= w) => SupportedPrimConstraint (IntN w) where
  type PrimConstraint (IntN w) = (KnownNat w, 1 <= w, BVIsNonZero w)

instance (KnownNat w, 1 <= w) => SBVRep (IntN w) where
  type SBVType (IntN w) = SBV.SBV (SBV.IntN w)

instance (KnownNat w, 1 <= w) => SupportedPrim (IntN w) where
  pformatCon :: IntN w -> String
pformatCon = IntN w -> String
forall a. Show a => a -> String
show
  defaultValue :: IntN w
defaultValue = IntN w
0
  pevalITETerm :: Term Bool -> Term (IntN w) -> Term (IntN w) -> Term (IntN w)
pevalITETerm = Term Bool -> Term (IntN w) -> Term (IntN w) -> Term (IntN w)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (IntN w) -> Term (IntN w) -> Term Bool
pevalEqTerm = Term (IntN w) -> Term (IntN w) -> Term Bool
forall a. SupportedNonFuncPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  pevalDistinctTerm :: NonEmpty (Term (IntN w)) -> Term Bool
pevalDistinctTerm = NonEmpty (Term (IntN w)) -> Term Bool
forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct
  conSBVTerm :: IntN w -> SBVType (IntN w)
conSBVTerm IntN w
n = Proxy w -> (BVIsNonZero w => SBVType (IntN w)) -> SBVType (IntN w)
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => SBVType (IntN w)) -> SBVType (IntN w))
-> (BVIsNonZero w => SBVType (IntN w)) -> SBVType (IntN w)
forall a b. (a -> b) -> a -> b
$ IntN w -> SBV (IntN w)
forall a b. (Integral a, Num b) => a -> b
fromIntegral IntN w
n
  symSBVName :: TypedSymbol 'AnyKind (IntN w) -> Int -> String
symSBVName TypedSymbol 'AnyKind (IntN w)
symbol Int
_ = TypedSymbol 'AnyKind (IntN w) -> String
forall a. Show a => a -> String
show TypedSymbol 'AnyKind (IntN w)
symbol
  symSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBVType (IntN w))
symSBVTerm String
name = Proxy w
-> (BVIsNonZero w => m (SBVType (IntN w))) -> m (SBVType (IntN w))
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => m (SBVType (IntN w))) -> m (SBVType (IntN w)))
-> (BVIsNonZero w => m (SBVType (IntN w))) -> m (SBVType (IntN w))
forall a b. (a -> b) -> a -> b
$ String -> m (SBV (IntN w))
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
  withPrim :: forall a.
((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
  Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
 a)
-> a
withPrim (PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
 Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
a
r = Proxy w -> (BVIsNonZero w => a) -> a
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) a
BVIsNonZero w => a
(PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
 Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
a
r
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> IntN w
parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv =
    forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(IntN w) (((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
   Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
  IntN w)
 -> IntN w)
-> ((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
     Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
    IntN w)
-> IntN w
forall a b. (a -> b) -> a -> b
$
      (IntN w -> IntN w) -> ([([CV], CV)], CV) -> IntN w
forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult (\(IntN w
x :: SBV.IntN w) -> IntN w -> IntN w
forall a b. (Integral a, Num b) => a -> b
fromIntegral IntN w
x) ([([CV], CV)], CV)
cv
  castTypedSymbol ::
    forall knd knd'.
    (IsSymbolKind knd') =>
    TypedSymbol knd (IntN w) ->
    Maybe (TypedSymbol knd' (IntN w))
  castTypedSymbol :: forall (knd :: SymbolKind) (knd' :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd (IntN w) -> Maybe (TypedSymbol knd' (IntN w))
castTypedSymbol (TypedSymbol Symbol
s) =
    case forall (ty :: SymbolKind).
IsSymbolKind ty =>
Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind)
decideSymbolKind @knd' of
      Left knd' :~~: 'ConstantKind
HRefl -> TypedSymbol knd' (IntN w) -> Maybe (TypedSymbol knd' (IntN w))
forall a. a -> Maybe a
Just (TypedSymbol knd' (IntN w) -> Maybe (TypedSymbol knd' (IntN w)))
-> TypedSymbol knd' (IntN w) -> Maybe (TypedSymbol knd' (IntN w))
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol knd' (IntN w)
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
s
      Right knd' :~~: 'AnyKind
HRefl -> TypedSymbol knd' (IntN w) -> Maybe (TypedSymbol knd' (IntN w))
forall a. a -> Maybe a
Just (TypedSymbol knd' (IntN w) -> Maybe (TypedSymbol knd' (IntN w)))
-> TypedSymbol knd' (IntN w) -> Maybe (TypedSymbol knd' (IntN w))
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol knd' (IntN w)
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
s
  isFuncType :: Bool
isFuncType = Bool
False
  funcDummyConstraint :: SBVType (IntN w) -> SBV Bool
funcDummyConstraint SBVType (IntN w)
_ = SBV Bool
SBV.sTrue

-- | Construct the 'SBV.BVIsNonZero' constraint from the proof that the width is
-- at least 1.
bvIsNonZeroFromGEq1 ::
  forall w r proxy.
  (1 <= w) =>
  proxy w ->
  ((SBV.BVIsNonZero w) => r) ->
  r
bvIsNonZeroFromGEq1 :: forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 proxy w
_ BVIsNonZero w => r
r1 = case w :~: 1
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: w :~: 1 of
  w :~: 1
Refl -> r
BVIsNonZero w => r
r1

instance (KnownNat w, 1 <= w) => NonFuncSBVRep (IntN w) where
  type NonFuncSBVBaseType (IntN w) = SBV.IntN w

instance (KnownNat w, 1 <= w) => SupportedNonFuncPrim (IntN w) where
  conNonFuncSBVTerm :: IntN w -> SBV (NonFuncSBVBaseType (IntN w))
conNonFuncSBVTerm = IntN w -> SBV (NonFuncSBVBaseType (IntN w))
IntN w -> SBVType (IntN w)
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBV (NonFuncSBVBaseType (IntN w)))
symNonFuncSBVTerm = forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
String -> m (SBVType t)
symSBVTerm @(IntN w)
  withNonFuncPrim :: forall r. (NonFuncPrimConstraint (IntN w) => r) -> r
withNonFuncPrim NonFuncPrimConstraint (IntN w) => r
r = Proxy w -> (BVIsNonZero w => r) -> r
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) r
NonFuncPrimConstraint (IntN w) => r
BVIsNonZero w => r
r

-- Unsigned BV
instance (KnownNat w, 1 <= w) => SupportedPrimConstraint (WordN w) where
  type PrimConstraint (WordN w) = (KnownNat w, 1 <= w, BVIsNonZero w)

instance (KnownNat w, 1 <= w) => SBVRep (WordN w) where
  type SBVType (WordN w) = SBV.SBV (SBV.WordN w)

instance (KnownNat w, 1 <= w) => SupportedPrim (WordN w) where
  pformatCon :: WordN w -> String
pformatCon = WordN w -> String
forall a. Show a => a -> String
show
  defaultValue :: WordN w
defaultValue = WordN w
0
  pevalITETerm :: Term Bool -> Term (WordN w) -> Term (WordN w) -> Term (WordN w)
pevalITETerm = Term Bool -> Term (WordN w) -> Term (WordN w) -> Term (WordN w)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (WordN w) -> Term (WordN w) -> Term Bool
pevalEqTerm = Term (WordN w) -> Term (WordN w) -> Term Bool
forall a. SupportedNonFuncPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  pevalDistinctTerm :: NonEmpty (Term (WordN w)) -> Term Bool
pevalDistinctTerm = NonEmpty (Term (WordN w)) -> Term Bool
forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct
  conSBVTerm :: WordN w -> SBVType (WordN w)
conSBVTerm WordN w
n = Proxy w
-> (BVIsNonZero w => SBVType (WordN w)) -> SBVType (WordN w)
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => SBVType (WordN w)) -> SBVType (WordN w))
-> (BVIsNonZero w => SBVType (WordN w)) -> SBVType (WordN w)
forall a b. (a -> b) -> a -> b
$ WordN w -> SBV (WordN w)
forall a b. (Integral a, Num b) => a -> b
fromIntegral WordN w
n
  symSBVName :: TypedSymbol 'AnyKind (WordN w) -> Int -> String
symSBVName TypedSymbol 'AnyKind (WordN w)
symbol Int
_ = TypedSymbol 'AnyKind (WordN w) -> String
forall a. Show a => a -> String
show TypedSymbol 'AnyKind (WordN w)
symbol
  symSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBVType (WordN w))
symSBVTerm String
name = Proxy w
-> (BVIsNonZero w => m (SBVType (WordN w)))
-> m (SBVType (WordN w))
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => m (SBVType (WordN w))) -> m (SBVType (WordN w)))
-> (BVIsNonZero w => m (SBVType (WordN w)))
-> m (SBVType (WordN w))
forall a b. (a -> b) -> a -> b
$ String -> m (SBV (WordN w))
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
  withPrim :: forall a.
((PrimConstraint (WordN w), SMTDefinable (SBVType (WordN w)),
  Mergeable (SBVType (WordN w)), Typeable (SBVType (WordN w))) =>
 a)
-> a
withPrim (PrimConstraint (WordN w), SMTDefinable (SBVType (WordN w)),
 Mergeable (SBVType (WordN w)), Typeable (SBVType (WordN w))) =>
a
r = Proxy w -> (BVIsNonZero w => a) -> a
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) a
BVIsNonZero w => a
(PrimConstraint (WordN w), SMTDefinable (SBVType (WordN w)),
 Mergeable (SBVType (WordN w)), Typeable (SBVType (WordN w))) =>
a
r
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> WordN w
parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv =
    forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(IntN w) (((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
   Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
  WordN w)
 -> WordN w)
-> ((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
     Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
    WordN w)
-> WordN w
forall a b. (a -> b) -> a -> b
$
      (WordN w -> WordN w) -> ([([CV], CV)], CV) -> WordN w
forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult (\(WordN w
x :: SBV.WordN w) -> WordN w -> WordN w
forall a b. (Integral a, Num b) => a -> b
fromIntegral WordN w
x) ([([CV], CV)], CV)
cv
  castTypedSymbol ::
    forall knd knd'.
    (IsSymbolKind knd') =>
    TypedSymbol knd (WordN w) ->
    Maybe (TypedSymbol knd' (WordN w))
  castTypedSymbol :: forall (knd :: SymbolKind) (knd' :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd (WordN w) -> Maybe (TypedSymbol knd' (WordN w))
castTypedSymbol (TypedSymbol Symbol
s) =
    case forall (ty :: SymbolKind).
IsSymbolKind ty =>
Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind)
decideSymbolKind @knd' of
      Left knd' :~~: 'ConstantKind
HRefl -> TypedSymbol knd' (WordN w) -> Maybe (TypedSymbol knd' (WordN w))
forall a. a -> Maybe a
Just (TypedSymbol knd' (WordN w) -> Maybe (TypedSymbol knd' (WordN w)))
-> TypedSymbol knd' (WordN w) -> Maybe (TypedSymbol knd' (WordN w))
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol knd' (WordN w)
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
s
      Right knd' :~~: 'AnyKind
HRefl -> TypedSymbol knd' (WordN w) -> Maybe (TypedSymbol knd' (WordN w))
forall a. a -> Maybe a
Just (TypedSymbol knd' (WordN w) -> Maybe (TypedSymbol knd' (WordN w)))
-> TypedSymbol knd' (WordN w) -> Maybe (TypedSymbol knd' (WordN w))
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol knd' (WordN w)
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
s
  isFuncType :: Bool
isFuncType = Bool
False
  funcDummyConstraint :: SBVType (WordN w) -> SBV Bool
funcDummyConstraint SBVType (WordN w)
_ = SBV Bool
SBV.sTrue

instance (KnownNat w, 1 <= w) => NonFuncSBVRep (WordN w) where
  type NonFuncSBVBaseType (WordN w) = SBV.WordN w

instance (KnownNat w, 1 <= w) => SupportedNonFuncPrim (WordN w) where
  conNonFuncSBVTerm :: WordN w -> SBV (NonFuncSBVBaseType (WordN w))
conNonFuncSBVTerm = WordN w -> SBV (NonFuncSBVBaseType (WordN w))
WordN w -> SBVType (WordN w)
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBV (NonFuncSBVBaseType (WordN w)))
symNonFuncSBVTerm = forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
String -> m (SBVType t)
symSBVTerm @(WordN w)
  withNonFuncPrim :: forall r. (NonFuncPrimConstraint (WordN w) => r) -> r
withNonFuncPrim NonFuncPrimConstraint (WordN w) => r
r = Proxy w -> (BVIsNonZero w => r) -> r
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) r
NonFuncPrimConstraint (WordN w) => r
BVIsNonZero w => r
r

-- FP
instance (ValidFP eb sb) => SupportedPrimConstraint (FP eb sb) where
  type PrimConstraint (FP eb sb) = ValidFP eb sb

instance (ValidFP eb sb) => SBVRep (FP eb sb) where
  type SBVType (FP eb sb) = SBV.SBV (SBV.FloatingPoint eb sb)

instance (ValidFP eb sb) => SupportedPrim (FP eb sb) where
  defaultValue :: FP eb sb
defaultValue = FP eb sb
0
  pevalITETerm :: Term Bool -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalITETerm = Term Bool -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
pevalEqTerm (ConTerm Int
_ FP eb sb
l) (ConTerm Int
_ FP eb sb
r) = Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ FP eb sb
l FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== FP eb sb
r
  pevalEqTerm l :: Term (FP eb sb)
l@ConTerm {} Term (FP eb sb)
r = Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term (FP eb sb)
r Term (FP eb sb)
l
  pevalEqTerm Term (FP eb sb)
l Term (FP eb sb)
r = Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall a. SupportedNonFuncPrim a => Term a -> Term a -> Term Bool
eqTerm Term (FP eb sb)
l Term (FP eb sb)
r
  pevalDistinctTerm :: NonEmpty (Term (FP eb sb)) -> Term Bool
pevalDistinctTerm = NonEmpty (Term (FP eb sb)) -> Term Bool
forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
distinctTerm
  conSBVTerm :: FP eb sb -> SBVType (FP eb sb)
conSBVTerm (FP FloatingPoint eb sb
fp) = FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
forall a. SymVal a => a -> SBV a
SBV.literal FloatingPoint eb sb
fp
  symSBVName :: TypedSymbol 'AnyKind (FP eb sb) -> Int -> String
symSBVName TypedSymbol 'AnyKind (FP eb sb)
symbol Int
_ = TypedSymbol 'AnyKind (FP eb sb) -> String
forall a. Show a => a -> String
show TypedSymbol 'AnyKind (FP eb sb)
symbol
  symSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBVType (FP eb sb))
symSBVTerm String
name = String -> m (SBV (FloatingPoint eb sb))
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
  withPrim :: forall a.
((PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
  Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
 a)
-> a
withPrim (PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
 Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
a
r = a
(PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
 Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
a
r
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FP eb sb
parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv =
    forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(FP eb sb) (((PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
   Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
  FP eb sb)
 -> FP eb sb)
-> ((PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
     Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$
      (FloatingPoint eb sb -> FP eb sb) -> ([([CV], CV)], CV) -> FP eb sb
forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult (\(FloatingPoint eb sb
x :: SBV.FloatingPoint eb sb) -> FloatingPoint eb sb -> FP eb sb
forall a b. Coercible a b => a -> b
coerce FloatingPoint eb sb
x) ([([CV], CV)], CV)
cv
  isFuncType :: Bool
isFuncType = Bool
False
  funcDummyConstraint :: SBVType (FP eb sb) -> SBV Bool
funcDummyConstraint SBVType (FP eb sb)
_ = SBV Bool
SBV.sTrue

  -- Workaround for sbv#702.
  sbvIte :: SBV Bool
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
sbvIte = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(FP eb sb) (((PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
   Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
  SBV Bool
  -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb))
 -> SBV Bool
 -> SBVType (FP eb sb)
 -> SBVType (FP eb sb)
 -> SBVType (FP eb sb))
-> ((PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
     Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
    SBV Bool
    -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb))
-> SBV Bool
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$ \SBV Bool
c SBVType (FP eb sb)
a SBVType (FP eb sb)
b ->
    case (SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
forall a. SymVal a => SBV a -> Maybe a
SBV.unliteral SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
a, SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
forall a. SymVal a => SBV a -> Maybe a
SBV.unliteral SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
b) of
      (Just FloatingPoint eb sb
a', Just FloatingPoint eb sb
b')
        | FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isInfinite FloatingPoint eb sb
a' Bool -> Bool -> Bool
&& FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isInfinite FloatingPoint eb sb
b' ->
            let correspondingZero :: a -> a
correspondingZero a
x = if a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 then a
0 else -a
0
             in SBV (FloatingPoint eb sb)
1
                  SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Fractional a => a -> a -> a
/ forall t.
SupportedPrim t =>
SBV Bool -> SBVType t -> SBVType t -> SBVType t
sbvIte @(FP eb sb)
                    SBV Bool
c
                    (forall t. SupportedPrim t => t -> SBVType t
conSBVTerm @(FP eb sb) (FP eb sb -> SBVType (FP eb sb)) -> FP eb sb -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FloatingPoint eb sb -> FP eb sb
forall {a} {a}. (Ord a, Num a, Num a) => a -> a
correspondingZero FloatingPoint eb sb
a')
                    (forall t. SupportedPrim t => t -> SBVType t
conSBVTerm @(FP eb sb) (FP eb sb -> SBVType (FP eb sb)) -> FP eb sb -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FloatingPoint eb sb -> FP eb sb
forall {a} {a}. (Ord a, Num a, Num a) => a -> a
correspondingZero FloatingPoint eb sb
b')
      (Maybe (FloatingPoint eb sb), Maybe (FloatingPoint eb sb))
_ -> SBV Bool
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite SBV Bool
c SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
a SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
b
  castTypedSymbol ::
    forall knd knd'.
    (IsSymbolKind knd') =>
    TypedSymbol knd (FP eb sb) ->
    Maybe (TypedSymbol knd' (FP eb sb))
  castTypedSymbol :: forall (knd :: SymbolKind) (knd' :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd (FP eb sb) -> Maybe (TypedSymbol knd' (FP eb sb))
castTypedSymbol (TypedSymbol Symbol
s) =
    case forall (ty :: SymbolKind).
IsSymbolKind ty =>
Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind)
decideSymbolKind @knd' of
      Left knd' :~~: 'ConstantKind
HRefl -> TypedSymbol knd' (FP eb sb) -> Maybe (TypedSymbol knd' (FP eb sb))
forall a. a -> Maybe a
Just (TypedSymbol knd' (FP eb sb)
 -> Maybe (TypedSymbol knd' (FP eb sb)))
-> TypedSymbol knd' (FP eb sb)
-> Maybe (TypedSymbol knd' (FP eb sb))
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol knd' (FP eb sb)
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
s
      Right knd' :~~: 'AnyKind
HRefl -> TypedSymbol knd' (FP eb sb) -> Maybe (TypedSymbol knd' (FP eb sb))
forall a. a -> Maybe a
Just (TypedSymbol knd' (FP eb sb)
 -> Maybe (TypedSymbol knd' (FP eb sb)))
-> TypedSymbol knd' (FP eb sb)
-> Maybe (TypedSymbol knd' (FP eb sb))
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol knd' (FP eb sb)
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
s

instance (ValidFP eb sb) => NonFuncSBVRep (FP eb sb) where
  type NonFuncSBVBaseType (FP eb sb) = SBV.FloatingPoint eb sb

instance (ValidFP eb sb) => SupportedNonFuncPrim (FP eb sb) where
  conNonFuncSBVTerm :: FP eb sb -> SBV (NonFuncSBVBaseType (FP eb sb))
conNonFuncSBVTerm = FP eb sb -> SBV (NonFuncSBVBaseType (FP eb sb))
FP eb sb -> SBVType (FP eb sb)
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBV (NonFuncSBVBaseType (FP eb sb)))
symNonFuncSBVTerm = forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
String -> m (SBVType t)
symSBVTerm @(FP eb sb)
  withNonFuncPrim :: forall r. (NonFuncPrimConstraint (FP eb sb) => r) -> r
withNonFuncPrim NonFuncPrimConstraint (FP eb sb) => r
r = r
NonFuncPrimConstraint (FP eb sb) => r
r

-- FPRoundingMode
instance SupportedPrimConstraint FPRoundingMode

instance SBVRep FPRoundingMode where
  type SBVType FPRoundingMode = SBV.SBV SBV.RoundingMode

instance SupportedPrim FPRoundingMode where
  defaultValue :: FPRoundingMode
defaultValue = FPRoundingMode
RNE
  pevalITETerm :: Term Bool
-> Term FPRoundingMode
-> Term FPRoundingMode
-> Term FPRoundingMode
pevalITETerm = Term Bool
-> Term FPRoundingMode
-> Term FPRoundingMode
-> Term FPRoundingMode
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
pevalEqTerm (ConTerm Int
_ FPRoundingMode
l) (ConTerm Int
_ FPRoundingMode
r) = Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ FPRoundingMode
l FPRoundingMode -> FPRoundingMode -> Bool
forall a. Eq a => a -> a -> Bool
== FPRoundingMode
r
  pevalEqTerm l :: Term FPRoundingMode
l@ConTerm {} Term FPRoundingMode
r = Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term FPRoundingMode
r Term FPRoundingMode
l
  pevalEqTerm Term FPRoundingMode
l Term FPRoundingMode
r = Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
forall a. SupportedNonFuncPrim a => Term a -> Term a -> Term Bool
eqTerm Term FPRoundingMode
l Term FPRoundingMode
r
  pevalDistinctTerm :: NonEmpty (Term FPRoundingMode) -> Term Bool
pevalDistinctTerm = NonEmpty (Term FPRoundingMode) -> Term Bool
forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct
  conSBVTerm :: FPRoundingMode -> SBVType FPRoundingMode
conSBVTerm FPRoundingMode
RNE = SBV RoundingMode
SBVType FPRoundingMode
SBV.sRNE
  conSBVTerm FPRoundingMode
RNA = SBV RoundingMode
SBVType FPRoundingMode
SBV.sRNA
  conSBVTerm FPRoundingMode
RTP = SBV RoundingMode
SBVType FPRoundingMode
SBV.sRTP
  conSBVTerm FPRoundingMode
RTN = SBV RoundingMode
SBVType FPRoundingMode
SBV.sRTN
  conSBVTerm FPRoundingMode
RTZ = SBV RoundingMode
SBVType FPRoundingMode
SBV.sRTZ
  symSBVName :: TypedSymbol 'AnyKind FPRoundingMode -> Int -> String
symSBVName TypedSymbol 'AnyKind FPRoundingMode
symbol Int
_ = TypedSymbol 'AnyKind FPRoundingMode -> String
forall a. Show a => a -> String
show TypedSymbol 'AnyKind FPRoundingMode
symbol
  symSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBVType FPRoundingMode)
symSBVTerm String
name = String -> m (SBV RoundingMode)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
  withPrim :: forall a.
((PrimConstraint FPRoundingMode,
  SMTDefinable (SBVType FPRoundingMode),
  Mergeable (SBVType FPRoundingMode),
  Typeable (SBVType FPRoundingMode)) =>
 a)
-> a
withPrim (PrimConstraint FPRoundingMode,
 SMTDefinable (SBVType FPRoundingMode),
 Mergeable (SBVType FPRoundingMode),
 Typeable (SBVType FPRoundingMode)) =>
a
r = a
(PrimConstraint FPRoundingMode,
 SMTDefinable (SBVType FPRoundingMode),
 Mergeable (SBVType FPRoundingMode),
 Typeable (SBVType FPRoundingMode)) =>
a
r
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FPRoundingMode
parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv =
    forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(FPRoundingMode) (((PrimConstraint FPRoundingMode,
   SMTDefinable (SBVType FPRoundingMode),
   Mergeable (SBVType FPRoundingMode),
   Typeable (SBVType FPRoundingMode)) =>
  FPRoundingMode)
 -> FPRoundingMode)
-> ((PrimConstraint FPRoundingMode,
     SMTDefinable (SBVType FPRoundingMode),
     Mergeable (SBVType FPRoundingMode),
     Typeable (SBVType FPRoundingMode)) =>
    FPRoundingMode)
-> FPRoundingMode
forall a b. (a -> b) -> a -> b
$
      (RoundingMode -> FPRoundingMode)
-> ([([CV], CV)], CV) -> FPRoundingMode
forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult
        ( \(RoundingMode
x :: SBV.RoundingMode) -> case RoundingMode
x of
            RoundingMode
SBV.RoundNearestTiesToEven -> FPRoundingMode
RNE
            RoundingMode
SBV.RoundNearestTiesToAway -> FPRoundingMode
RNA
            RoundingMode
SBV.RoundTowardPositive -> FPRoundingMode
RTP
            RoundingMode
SBV.RoundTowardNegative -> FPRoundingMode
RTN
            RoundingMode
SBV.RoundTowardZero -> FPRoundingMode
RTZ
        )
        ([([CV], CV)], CV)
cv
  castTypedSymbol ::
    forall knd knd'.
    (IsSymbolKind knd') =>
    TypedSymbol knd FPRoundingMode ->
    Maybe (TypedSymbol knd' FPRoundingMode)
  castTypedSymbol :: forall (knd :: SymbolKind) (knd' :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd FPRoundingMode
-> Maybe (TypedSymbol knd' FPRoundingMode)
castTypedSymbol (TypedSymbol Symbol
s) =
    case forall (ty :: SymbolKind).
IsSymbolKind ty =>
Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind)
decideSymbolKind @knd' of
      Left knd' :~~: 'ConstantKind
HRefl -> TypedSymbol knd' FPRoundingMode
-> Maybe (TypedSymbol knd' FPRoundingMode)
forall a. a -> Maybe a
Just (TypedSymbol knd' FPRoundingMode
 -> Maybe (TypedSymbol knd' FPRoundingMode))
-> TypedSymbol knd' FPRoundingMode
-> Maybe (TypedSymbol knd' FPRoundingMode)
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol knd' FPRoundingMode
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
s
      Right knd' :~~: 'AnyKind
HRefl -> TypedSymbol knd' FPRoundingMode
-> Maybe (TypedSymbol knd' FPRoundingMode)
forall a. a -> Maybe a
Just (TypedSymbol knd' FPRoundingMode
 -> Maybe (TypedSymbol knd' FPRoundingMode))
-> TypedSymbol knd' FPRoundingMode
-> Maybe (TypedSymbol knd' FPRoundingMode)
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol knd' FPRoundingMode
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
s
  isFuncType :: Bool
isFuncType = Bool
False
  funcDummyConstraint :: SBVType FPRoundingMode -> SBV Bool
funcDummyConstraint SBVType FPRoundingMode
_ = SBV Bool
SBV.sTrue

instance NonFuncSBVRep FPRoundingMode where
  type NonFuncSBVBaseType FPRoundingMode = SBV.RoundingMode

instance SupportedNonFuncPrim FPRoundingMode where
  conNonFuncSBVTerm :: FPRoundingMode -> SBV (NonFuncSBVBaseType FPRoundingMode)
conNonFuncSBVTerm = FPRoundingMode -> SBV (NonFuncSBVBaseType FPRoundingMode)
FPRoundingMode -> SBVType FPRoundingMode
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBV (NonFuncSBVBaseType FPRoundingMode))
symNonFuncSBVTerm = forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
String -> m (SBVType t)
symSBVTerm @FPRoundingMode
  withNonFuncPrim :: forall r. (NonFuncPrimConstraint FPRoundingMode => r) -> r
withNonFuncPrim NonFuncPrimConstraint FPRoundingMode => r
r = r
NonFuncPrimConstraint FPRoundingMode => r
r

-- AlgReal

instance SupportedPrimConstraint AlgReal

instance SBVRep AlgReal where
  type SBVType AlgReal = SBV.SBV SBV.AlgReal

instance SupportedPrim AlgReal where
  defaultValue :: AlgReal
defaultValue = AlgReal
0
  pevalITETerm :: Term Bool -> Term AlgReal -> Term AlgReal -> Term AlgReal
pevalITETerm = Term Bool -> Term AlgReal -> Term AlgReal -> Term AlgReal
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term AlgReal -> Term AlgReal -> Term Bool
pevalEqTerm (ConTerm Int
_ AlgReal
l) (ConTerm Int
_ AlgReal
r) = Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ AlgReal
l AlgReal -> AlgReal -> Bool
forall a. Eq a => a -> a -> Bool
== AlgReal
r
  pevalEqTerm l :: Term AlgReal
l@ConTerm {} Term AlgReal
r = Term AlgReal -> Term AlgReal -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term AlgReal
r Term AlgReal
l
  pevalEqTerm Term AlgReal
l Term AlgReal
r = Term AlgReal -> Term AlgReal -> Term Bool
forall a. SupportedNonFuncPrim a => Term a -> Term a -> Term Bool
eqTerm Term AlgReal
l Term AlgReal
r
  pevalDistinctTerm :: NonEmpty (Term AlgReal) -> Term Bool
pevalDistinctTerm = NonEmpty (Term AlgReal) -> Term Bool
forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct
  conSBVTerm :: AlgReal -> SBVType AlgReal
conSBVTerm = AlgReal -> SBV AlgReal
forall a. SymVal a => a -> SBV a
SBV.literal (AlgReal -> SBV AlgReal)
-> (AlgReal -> AlgReal) -> AlgReal -> SBV AlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlgReal -> AlgReal
toSBVAlgReal
  symSBVName :: TypedSymbol 'AnyKind AlgReal -> Int -> String
symSBVName TypedSymbol 'AnyKind AlgReal
symbol Int
_ = TypedSymbol 'AnyKind AlgReal -> String
forall a. Show a => a -> String
show TypedSymbol 'AnyKind AlgReal
symbol
  symSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBVType AlgReal)
symSBVTerm String
name = String -> m (SBV AlgReal)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
  withPrim :: forall a.
((PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal),
  Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) =>
 a)
-> a
withPrim (PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal),
 Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) =>
a
r = a
(PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal),
 Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) =>
a
r
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> AlgReal
parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv =
    forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @AlgReal (((PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal),
   Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) =>
  AlgReal)
 -> AlgReal)
-> ((PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal),
     Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) =>
    AlgReal)
-> AlgReal
forall a b. (a -> b) -> a -> b
$
      (AlgReal -> AlgReal) -> ([([CV], CV)], CV) -> AlgReal
forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult AlgReal -> AlgReal
fromSBVAlgReal ([([CV], CV)], CV)
cv
  castTypedSymbol ::
    forall knd knd'.
    (IsSymbolKind knd') =>
    TypedSymbol knd AlgReal ->
    Maybe (TypedSymbol knd' AlgReal)
  castTypedSymbol :: forall (knd :: SymbolKind) (knd' :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd AlgReal -> Maybe (TypedSymbol knd' AlgReal)
castTypedSymbol (TypedSymbol Symbol
s) =
    case forall (ty :: SymbolKind).
IsSymbolKind ty =>
Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind)
decideSymbolKind @knd' of
      Left knd' :~~: 'ConstantKind
HRefl -> TypedSymbol knd' AlgReal -> Maybe (TypedSymbol knd' AlgReal)
forall a. a -> Maybe a
Just (TypedSymbol knd' AlgReal -> Maybe (TypedSymbol knd' AlgReal))
-> TypedSymbol knd' AlgReal -> Maybe (TypedSymbol knd' AlgReal)
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol knd' AlgReal
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
s
      Right knd' :~~: 'AnyKind
HRefl -> TypedSymbol knd' AlgReal -> Maybe (TypedSymbol knd' AlgReal)
forall a. a -> Maybe a
Just (TypedSymbol knd' AlgReal -> Maybe (TypedSymbol knd' AlgReal))
-> TypedSymbol knd' AlgReal -> Maybe (TypedSymbol knd' AlgReal)
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol knd' AlgReal
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
s
  isFuncType :: Bool
isFuncType = Bool
False
  funcDummyConstraint :: SBVType AlgReal -> SBV Bool
funcDummyConstraint SBVType AlgReal
_ = SBV Bool
SBV.sTrue

instance NonFuncSBVRep AlgReal where
  type NonFuncSBVBaseType AlgReal = SBV.AlgReal

instance SupportedNonFuncPrim AlgReal where
  conNonFuncSBVTerm :: AlgReal -> SBV (NonFuncSBVBaseType AlgReal)
conNonFuncSBVTerm = AlgReal -> SBV (NonFuncSBVBaseType AlgReal)
AlgReal -> SBVType AlgReal
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBV (NonFuncSBVBaseType AlgReal))
symNonFuncSBVTerm = forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
String -> m (SBVType t)
symSBVTerm @AlgReal
  withNonFuncPrim :: forall r. (NonFuncPrimConstraint AlgReal => r) -> r
withNonFuncPrim NonFuncPrimConstraint AlgReal => r
r = r
NonFuncPrimConstraint AlgReal => r
r