copilot-verifier-4.3: System for verifying the correctness of generated Copilot programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

Copilot.Verifier.FloatMode

Synopsis

Documentation

data FloatMode Source #

How the verifier should interpret floating-point operations.

Constructors

FloatUninterpreted

Floating-point values are treated as bitvectors of the appropriate width, and all operations on them are translated as uninterpreted functions. This is the verifier's default interpretation, and it is what allows the verifier to perform any reasoning at all over floating-point operations that are not native to SMT-LIB (sin, cos, tan, etc.).

FloatIEEE

Floating-point values are treated as bit-precise IEEE-754 floats. This interpretation can perform deeper reasoning about floating-point operations that are native to SMT-LIB, but at the expense of causing the verifier to throw an error if it encounters operations that are not native to SMT-LIB (sin, cos, tan, etc.). Use at your own risk.

Instances

Instances details
Show FloatMode Source # 
Instance details

Defined in Copilot.Verifier.FloatMode

Methods

showsPrec :: Int -> FloatMode -> ShowS #

show :: FloatMode -> String #

showList :: [FloatMode] -> ShowS #

withFloatMode :: FloatMode -> (forall fm. FloatModeRepr fm -> r) -> r Source #

Convert a FloatMode into a What4 FloatModeRepr and pass it to a continuation.

withInterpretedFloatExprBuilder :: ExprBuilder t st (Flags fm) -> FloatModeRepr fm -> (IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags fm)) => r) -> r Source #

Match on a FloatModeRepr, compute evidence that it gives rise to an instance of IsInterpretedFloatExprBuilder, and pass the evidence to a continutation.