Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Safe-Inferred
Language	Haskell2010

Grisette.Internal.Backend.SBV

Description

Documentation

lowerSinglePrim :: forall integerBitWidth a m. (HasCallStack, SBVFreshMonad m) => GrisetteSMTConfig integerBitWidth -> Term a -> m (SymBiMap, TermTy integerBitWidth a) Source #

parseModel :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model Source #

type family TermTy bitWidth b where ... Source #

Equations

TermTy _ Bool = SBool
TermTy n Integer = Aux (IsZero n) n
TermTy n (IntN x) = SBV (IntN x)
TermTy n (WordN x) = SBV (WordN x)
TermTy n (a =-> b) = TermTy n a -> TermTy n b
TermTy n (a --> b) = TermTy n a -> TermTy n b
TermTy _ v = v