{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm
-- 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.PEvalOrdTerm
  ( pevalGeneralLtOrdTerm,
    pevalGeneralLeOrdTerm,
  )
where

import Control.Monad (msum)
import qualified Data.SBV as SBV
import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP
  ( FP,
    FPRoundingMode,
    ValidFP,
    allFPRoundingMode,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm ()
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalNumTerm (pevalNegNumTerm),
    PEvalOrdTerm
      ( pevalLeOrdTerm,
        pevalLtOrdTerm,
        sbvLeOrdTerm,
        sbvLtOrdTerm,
        withSbvOrdTermConstraint
      ),
    SupportedPrim (conSBVTerm, withPrim),
    Term,
    conTerm,
    leOrdTerm,
    ltOrdTerm,
    pevalSubNumTerm,
    pattern AddNumTerm,
    pattern ConTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (binaryUnfoldOnce)

-- | General partially evaluation of less than operation.
pevalGeneralLtOrdTerm :: (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm :: forall a. (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm = PartialRuleBinary a a Bool
-> TotalRuleBinary a a Bool -> TotalRuleBinary a a Bool
forall a b c.
SupportedPrim c =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a Bool
forall a.
(PEvalOrdTerm a, Ord a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLtOrdTerm TotalRuleBinary a a Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
ltOrdTerm

doPevalGeneralLtOrdTerm ::
  (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLtOrdTerm :: forall a.
(PEvalOrdTerm a, Ord a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLtOrdTerm (ConTerm a
a) (ConTerm a
b) = Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
b
doPevalGeneralLtOrdTerm Term a
_ Term a
_ = Maybe (Term Bool)
forall a. Maybe a
Nothing

-- | General partially evaluation of less than or equal to operation.
pevalGeneralLeOrdTerm :: (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm :: forall a. (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm = PartialRuleBinary a a Bool
-> TotalRuleBinary a a Bool -> TotalRuleBinary a a Bool
forall a b c.
SupportedPrim c =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a Bool
forall a.
(PEvalOrdTerm a, Ord a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLeOrdTerm TotalRuleBinary a a Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
leOrdTerm

doPevalGeneralLeOrdTerm ::
  (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLeOrdTerm :: forall a.
(PEvalOrdTerm a, Ord a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLeOrdTerm (ConTerm a
a) (ConTerm a
b) = Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b
doPevalGeneralLeOrdTerm Term a
_ Term a
_ = Maybe (Term Bool)
forall a. Maybe a
Nothing

instance PEvalOrdTerm Integer where
  pevalLtOrdTerm :: Term Integer -> Term Integer -> Term Bool
pevalLtOrdTerm = PartialRuleBinary Integer Integer Bool
-> (Term Integer -> Term Integer -> Term Bool)
-> Term Integer
-> Term Integer
-> Term Bool
forall a b c.
SupportedPrim c =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary Integer Integer Bool
forall {t}.
(Ord t, PEvalOrdTerm t, PEvalNumTerm t) =>
Term t -> Term t -> Maybe (Term Bool)
doPevalLtOrdTerm Term Integer -> Term Integer -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
ltOrdTerm
    where
      doPevalLtOrdTerm :: Term t -> Term t -> Maybe (Term Bool)
doPevalLtOrdTerm Term t
l Term t
r =
        [Maybe (Term Bool)] -> Maybe (Term Bool)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
          [ Term t -> Term t -> Maybe (Term Bool)
forall a.
(PEvalOrdTerm a, Ord a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLtOrdTerm Term t
l Term t
r,
            case (Term t
l, Term t
r) of
              (ConTerm t
l, AddNumTerm (ConTerm t
j) Term t
k) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm (t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t -> Term t) -> t -> Term t
forall a b. (a -> b) -> a -> b
$ t
l t -> t -> t
forall a. Num a => a -> a -> a
- t
j) Term t
k
              (AddNumTerm (ConTerm t
i) Term t
j, ConTerm t
k) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm Term t
j (t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t -> Term t) -> t -> Term t
forall a b. (a -> b) -> a -> b
$ t
k t -> t -> t
forall a. Num a => a -> a -> a
- t
i)
              ((AddNumTerm (ConTerm t
j) Term t
k), Term t
l) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$
                  Term t -> Term t -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm
                    (t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm t
j)
                    (Term t -> Term t -> Term t
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term t
l Term t
k)
              (Term t
j, (AddNumTerm (ConTerm t
k) Term t
l)) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm (t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t -> Term t) -> t -> Term t
forall a b. (a -> b) -> a -> b
$ -t
k) (Term t -> Term t -> Term t
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term t
l Term t
j)
              (Term t
l, ConTerm t
r) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm (t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t -> Term t) -> t -> Term t
forall a b. (a -> b) -> a -> b
$ -t
r) (Term t -> Term t
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term t
l)
              (Term t, Term t)
_ -> Maybe (Term Bool)
forall a. Maybe a
Nothing
          ]
  pevalLeOrdTerm :: Term Integer -> Term Integer -> Term Bool
pevalLeOrdTerm = PartialRuleBinary Integer Integer Bool
-> (Term Integer -> Term Integer -> Term Bool)
-> Term Integer
-> Term Integer
-> Term Bool
forall a b c.
SupportedPrim c =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary Integer Integer Bool
forall {t}.
(Ord t, PEvalOrdTerm t, PEvalNumTerm t) =>
Term t -> Term t -> Maybe (Term Bool)
doPevalLeOrdTerm Term Integer -> Term Integer -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
leOrdTerm
    where
      doPevalLeOrdTerm :: Term t -> Term t -> Maybe (Term Bool)
doPevalLeOrdTerm Term t
l Term t
r =
        [Maybe (Term Bool)] -> Maybe (Term Bool)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
          [ Term t -> Term t -> Maybe (Term Bool)
forall a.
(PEvalOrdTerm a, Ord a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLeOrdTerm Term t
l Term t
r,
            case (Term t
l, Term t
r) of
              (ConTerm t
l, AddNumTerm (ConTerm t
j) Term t
k) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm (t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t -> Term t) -> t -> Term t
forall a b. (a -> b) -> a -> b
$ t
l t -> t -> t
forall a. Num a => a -> a -> a
- t
j) Term t
k
              (AddNumTerm (ConTerm t
i) Term t
j, ConTerm t
k) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm Term t
j (t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t -> Term t) -> t -> Term t
forall a b. (a -> b) -> a -> b
$ t
k t -> t -> t
forall a. Num a => a -> a -> a
- t
i)
              (AddNumTerm (ConTerm t
j) Term t
k, Term t
l) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm (t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm t
j) (Term t -> Term t -> Term t
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term t
l Term t
k)
              (Term t
j, AddNumTerm (ConTerm t
k) Term t
l) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm (t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t -> Term t) -> t -> Term t
forall a b. (a -> b) -> a -> b
$ -t
k) (Term t -> Term t -> Term t
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term t
l Term t
j)
              (Term t
l, ConTerm t
r) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm (t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t -> Term t) -> t -> Term t
forall a b. (a -> b) -> a -> b
$ -t
r) (Term t -> Term t
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term t
l)
              (Term t, Term t)
_ -> Maybe (Term Bool)
forall a. Maybe a
Nothing
          ]
  withSbvOrdTermConstraint :: forall r. (OrdSymbolic (SBVType Integer) => r) -> r
withSbvOrdTermConstraint OrdSymbolic (SBVType Integer) => r
r = r
OrdSymbolic (SBVType Integer) => r
r

instance (KnownNat n, 1 <= n) => PEvalOrdTerm (WordN n) where
  pevalLtOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool
pevalLtOrdTerm = Term (WordN n) -> Term (WordN n) -> Term Bool
forall a. (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm
  pevalLeOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool
pevalLeOrdTerm = Term (WordN n) -> Term (WordN n) -> Term Bool
forall a. (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm
  withSbvOrdTermConstraint :: forall r. (OrdSymbolic (SBVType (WordN n)) => r) -> r
withSbvOrdTermConstraint OrdSymbolic (SBVType (WordN n)) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(WordN n) r
OrdSymbolic (SBVType (WordN n)) => r
(PrimConstraint (WordN n), SMTDefinable (SBVType (WordN n)),
 Mergeable (SBVType (WordN n)), Typeable (SBVType (WordN n))) =>
r
r

instance (KnownNat n, 1 <= n) => PEvalOrdTerm (IntN n) where
  pevalLtOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool
pevalLtOrdTerm = Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm
  pevalLeOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool
pevalLeOrdTerm = Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm
  withSbvOrdTermConstraint :: forall r. (OrdSymbolic (SBVType (IntN n)) => r) -> r
withSbvOrdTermConstraint OrdSymbolic (SBVType (IntN n)) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(IntN n) r
OrdSymbolic (SBVType (IntN n)) => r
(PrimConstraint (IntN n), SMTDefinable (SBVType (IntN n)),
 Mergeable (SBVType (IntN n)), Typeable (SBVType (IntN n))) =>
r
r

instance (ValidFP eb sb) => PEvalOrdTerm (FP eb sb) where
  pevalLtOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
pevalLtOrdTerm = Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall a. (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm
  pevalLeOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
pevalLeOrdTerm = Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall a. (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm
  withSbvOrdTermConstraint :: forall r. (OrdSymbolic (SBVType (FP eb sb)) => r) -> r
withSbvOrdTermConstraint OrdSymbolic (SBVType (FP eb sb)) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(FP eb sb) r
OrdSymbolic (SBVType (FP eb sb)) => r
(PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
 Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
r
r
  sbvLeOrdTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool
sbvLeOrdTerm SBVType (FP eb sb)
x SBVType (FP eb sb)
y =
    (SBV Bool -> SBV Bool
SBV.sNot (SBV (FloatingPoint eb sb) -> SBV Bool
forall a. IEEEFloating a => SBV a -> SBV Bool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x) SBV Bool -> SBV Bool -> SBV Bool
SBV..&& SBV Bool -> SBV Bool
SBV.sNot (SBV (FloatingPoint eb sb) -> SBV Bool
forall a. IEEEFloating a => SBV a -> SBV Bool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y))
      SBV Bool -> SBV Bool -> SBV Bool
SBV..&& (SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
x SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
SBV..<= SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
y)

-- Use this table to avoid accidental breakage introduced by sbv.
fpRoundingModeLtTable :: [(SBV.SRoundingMode, SBV.SRoundingMode)]
fpRoundingModeLtTable :: [(SRoundingMode, SRoundingMode)]
fpRoundingModeLtTable =
  [ ( forall t. SupportedPrim t => t -> SBVType t
conSBVTerm @FPRoundingMode FPRoundingMode
a,
      forall t. SupportedPrim t => t -> SBVType t
conSBVTerm @FPRoundingMode FPRoundingMode
b
    )
  | FPRoundingMode
a <- [FPRoundingMode]
allFPRoundingMode,
    FPRoundingMode
b <- [FPRoundingMode]
allFPRoundingMode,
    FPRoundingMode
a FPRoundingMode -> FPRoundingMode -> Bool
forall a. Ord a => a -> a -> Bool
< FPRoundingMode
b
  ]

fpRoundingModeLeTable :: [(SBV.SRoundingMode, SBV.SRoundingMode)]
fpRoundingModeLeTable :: [(SRoundingMode, SRoundingMode)]
fpRoundingModeLeTable =
  [ ( forall t. SupportedPrim t => t -> SBVType t
conSBVTerm @FPRoundingMode FPRoundingMode
a,
      forall t. SupportedPrim t => t -> SBVType t
conSBVTerm @FPRoundingMode FPRoundingMode
b
    )
  | FPRoundingMode
a <- [FPRoundingMode]
allFPRoundingMode,
    FPRoundingMode
b <- [FPRoundingMode]
allFPRoundingMode,
    FPRoundingMode
a FPRoundingMode -> FPRoundingMode -> Bool
forall a. Ord a => a -> a -> Bool
<= FPRoundingMode
b
  ]

sbvTableLookup ::
  [(SBV.SRoundingMode, SBV.SRoundingMode)] ->
  SBV.SRoundingMode ->
  SBV.SRoundingMode ->
  SBV.SBV Bool
sbvTableLookup :: [(SRoundingMode, SRoundingMode)]
-> SRoundingMode -> SRoundingMode -> SBV Bool
sbvTableLookup [(SRoundingMode, SRoundingMode)]
tbl SRoundingMode
lhs SRoundingMode
rhs =
  (SBV Bool -> (SRoundingMode, SRoundingMode) -> SBV Bool)
-> SBV Bool -> [(SRoundingMode, SRoundingMode)] -> SBV Bool
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
    (\SBV Bool
acc (SRoundingMode
a, SRoundingMode
b) -> SBV Bool
acc SBV Bool -> SBV Bool -> SBV Bool
SBV..|| ((SRoundingMode
lhs SRoundingMode -> SRoundingMode -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
SBV..== SRoundingMode
a) SBV Bool -> SBV Bool -> SBV Bool
SBV..&& (SRoundingMode
rhs SRoundingMode -> SRoundingMode -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
SBV..== SRoundingMode
b)))
    SBV Bool
SBV.sFalse
    [(SRoundingMode, SRoundingMode)]
tbl

instance PEvalOrdTerm FPRoundingMode where
  pevalLtOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
pevalLtOrdTerm = Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
forall a. (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm
  pevalLeOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
pevalLeOrdTerm = Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
forall a. (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm
  withSbvOrdTermConstraint :: forall r. (OrdSymbolic (SBVType FPRoundingMode) => r) -> r
withSbvOrdTermConstraint OrdSymbolic (SBVType FPRoundingMode) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @FPRoundingMode r
OrdSymbolic (SBVType FPRoundingMode) => r
(PrimConstraint FPRoundingMode,
 SMTDefinable (SBVType FPRoundingMode),
 Mergeable (SBVType FPRoundingMode),
 Typeable (SBVType FPRoundingMode)) =>
r
r
  sbvLtOrdTerm :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool
sbvLtOrdTerm = [(SRoundingMode, SRoundingMode)]
-> SRoundingMode -> SRoundingMode -> SBV Bool
sbvTableLookup [(SRoundingMode, SRoundingMode)]
fpRoundingModeLtTable
  sbvLeOrdTerm :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool
sbvLeOrdTerm = [(SRoundingMode, SRoundingMode)]
-> SRoundingMode -> SRoundingMode -> SBV Bool
sbvTableLookup [(SRoundingMode, SRoundingMode)]
fpRoundingModeLeTable

instance PEvalOrdTerm AlgReal where
  pevalLtOrdTerm :: Term AlgReal -> Term AlgReal -> Term Bool
pevalLtOrdTerm = Term AlgReal -> Term AlgReal -> Term Bool
forall a. (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm
  pevalLeOrdTerm :: Term AlgReal -> Term AlgReal -> Term Bool
pevalLeOrdTerm = Term AlgReal -> Term AlgReal -> Term Bool
forall a. (PEvalOrdTerm a, Ord a) => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm
  withSbvOrdTermConstraint :: forall r. (OrdSymbolic (SBVType AlgReal) => r) -> r
withSbvOrdTermConstraint OrdSymbolic (SBVType AlgReal) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @AlgReal r
OrdSymbolic (SBVType AlgReal) => r
(PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal),
 Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) =>
r
r