grisette-0.1.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellSafe-Inferred
LanguageHaskell2010

Grisette.Internal.Backend.SBV

Description

 

Documentation

lowerSinglePrim :: forall integerBitWidth a. HasCallStack => GrisetteSMTConfig integerBitWidth -> Term a -> Symbolic (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