what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2016-2020
License | BSD3
Maintainer | Joe Hendrix <jhendrix@galois.com>
Safe Haskell | None
Language | Haskell2010

What4.Expr.MATLAB

Contents

- Utilities for definition

Description

This module provides an interface that a symbolic backend should implement to support MATLAB intrinsics.

Synopsis

- data MatlabSolverFn (f :: BaseType -> Type) (args :: Ctx BaseType) (ret :: BaseType) where
  - BoolOrFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBoolType) '::> BaseBoolType) 'BaseBoolType
  - IsIntegerFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseBoolType
  - IntLeFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseIntegerType) '::> BaseIntegerType) 'BaseBoolType
  - BVToIntegerFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) 'BaseIntegerType
  - SBVToIntegerFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) 'BaseIntegerType
  - IntegerToRealFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseIntegerType) 'BaseRealType
  - RealToIntegerFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseIntegerType
  - PredToIntegerFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBoolType) 'BaseIntegerType
  - IntSeqFn :: forall (f :: BaseType -> Type). !(f BaseIntegerType) -> !(f BaseIntegerType) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseIntegerType) '::> BaseIntegerType) 'BaseIntegerType
  - RealSeqFn :: forall (f :: BaseType -> Type). !(f BaseRealType) -> !(f BaseRealType) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseIntegerType) '::> BaseIntegerType) 'BaseRealType
  - IndicesInRange :: forall (idx :: Ctx BaseType) (itp :: BaseType) (f :: BaseType -> Type). !(Assignment OnlyIntRepr (idx ::> itp)) -> !(Assignment f (idx ::> itp)) -> MatlabSolverFn f (idx '::> itp) 'BaseBoolType
  - IsEqFn :: forall (tp :: BaseType) (f :: BaseType -> Type). !(BaseTypeRepr tp) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> tp) '::> tp) 'BaseBoolType
  - BVIsNonZeroFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) 'BaseBoolType
  - ClampedIntNegFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) ('BaseBVType w)
  - ClampedIntAbsFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) ('BaseBVType w)
  - ClampedIntAddFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w)
  - ClampedIntSubFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w)
  - ClampedIntMulFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w)
  - ClampedUIntAddFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w)
  - ClampedUIntSubFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w)
  - ClampedUIntMulFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w)
  - IntSetWidthFn :: forall (m :: Natural) (n :: Natural) (f :: BaseType -> Type). (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType m) ('BaseBVType n)
  - UIntSetWidthFn :: forall (m :: Natural) (n :: Natural) (f :: BaseType -> Type). (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType m) ('BaseBVType n)
  - UIntToIntFn :: forall (m :: Natural) (n :: Natural) (f :: BaseType -> Type). (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType m) ('BaseBVType n)
  - IntToUIntFn :: forall (m :: Natural) (n :: Natural) (f :: BaseType -> Type). (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType m) ('BaseBVType n)
  - RealIsNonZeroFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseBoolType
  - RealCosFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseRealType
  - RealSinFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseRealType
  - RealToSBVFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) ('BaseBVType w)
  - RealToUBVFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) ('BaseBVType w)
  - PredToBVFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBoolType) ('BaseBVType w)
  - CplxIsNonZeroFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseBoolType
  - CplxIsRealFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseBoolType
  - RealToComplexFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseComplexType
  - RealPartOfCplxFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseRealType
  - ImagPartOfCplxFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseRealType
  - CplxNegFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
  - CplxAddFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseComplexType) '::> BaseComplexType) 'BaseComplexType
  - CplxSubFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseComplexType) '::> BaseComplexType) 'BaseComplexType
  - CplxMulFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseComplexType) '::> BaseComplexType) 'BaseComplexType
  - CplxRoundFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
  - CplxFloorFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
  - CplxCeilFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
  - CplxMagFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseRealType
  - CplxSqrtFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
  - CplxExpFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
  - CplxLogFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
  - CplxLogBaseFn :: forall (f :: BaseType -> Type). !Integer -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
  - CplxSinFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
  - CplxCosFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
  - CplxTanFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
- matlabSolverArgTypes :: forall (f :: BaseType -> Type) (args :: Ctx BaseType) (ret :: BaseType). MatlabSolverFn f args ret -> Assignment BaseTypeRepr args
- matlabSolverReturnType :: forall (f :: BaseType -> Type) (args :: Ctx BaseType) (ret :: BaseType). MatlabSolverFn f args ret -> BaseTypeRepr ret
- ppMatlabSolverFn :: forall (f :: BaseType -> Type) (a :: Ctx BaseType) (r :: BaseType) ann. IsExpr f => MatlabSolverFn f a r -> Doc ann
- evalMatlabSolverFn :: forall sym (args :: Ctx BaseType) (ret :: BaseType). IsExprBuilder sym => MatlabSolverFn (SymExpr sym) args ret -> sym -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
- testSolverFnEq :: forall (f :: BaseType -> Type) (ax :: Ctx BaseType) (rx :: BaseType) (ay :: Ctx BaseType) (ry :: BaseType). TestEquality f => MatlabSolverFn f ax rx -> MatlabSolverFn f ay ry -> Maybe ((ax ::> rx) :~: (ay ::> ry))
- traverseMatlabSolverFn :: forall m e f (a :: Ctx BaseType) (r :: BaseType). Applicative m => (forall (tp :: BaseType). e tp -> m (f tp)) -> MatlabSolverFn e a r -> m (MatlabSolverFn f a r)
- class IsSymExprBuilder sym => MatlabSymbolicArrayBuilder sym where
  - mkMatlabSolverFn :: forall (args :: Ctx BaseType) (ret :: BaseType). sym -> MatlabSolverFn (SymExpr sym) args ret -> IO (SymFn sym args ret)
- clampedIntAdd :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedIntSub :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedIntMul :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedIntNeg :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
- clampedIntAbs :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
- clampedUIntAdd :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedUIntSub :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedUIntMul :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

# Documentation

data MatlabSolverFn (f :: BaseType -> Type) (args :: Ctx BaseType) (ret :: BaseType) where Source #

Builtin functions that can be used to generate symbolic functions.

These functions are expected to be total, but the value returned may not be specified. e.g. `IntegerToNatFn` must return some natural number for every integer, but for negative integers, the particular number is unspecified.

Constructors

BoolOrFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBoolType) '::> BaseBoolType) 'BaseBoolType |
IsIntegerFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseBoolType |
IntLeFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseIntegerType) '::> BaseIntegerType) 'BaseBoolType |
BVToIntegerFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) 'BaseIntegerType |
SBVToIntegerFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) 'BaseIntegerType |
IntegerToRealFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseIntegerType) 'BaseRealType |
RealToIntegerFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseIntegerType |
PredToIntegerFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBoolType) 'BaseIntegerType |
IntSeqFn :: forall (f :: BaseType -> Type). !(f BaseIntegerType) -> !(f BaseIntegerType) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseIntegerType) '::> BaseIntegerType) 'BaseIntegerType |
RealSeqFn :: forall (f :: BaseType -> Type). !(f BaseRealType) -> !(f BaseRealType) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseIntegerType) '::> BaseIntegerType) 'BaseRealType |
IndicesInRange :: forall (idx :: Ctx BaseType) (itp :: BaseType) (f :: BaseType -> Type). !(Assignment OnlyIntRepr (idx ::> itp)) -> !(Assignment f (idx ::> itp)) -> MatlabSolverFn f (idx '::> itp) 'BaseBoolType |
IsEqFn :: forall (tp :: BaseType) (f :: BaseType -> Type). !(BaseTypeRepr tp) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> tp) '::> tp) 'BaseBoolType |
BVIsNonZeroFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) 'BaseBoolType |
ClampedIntNegFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) ('BaseBVType w) |
ClampedIntAbsFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) ('BaseBVType w) |
ClampedIntAddFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w) |
ClampedIntSubFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w) |
ClampedIntMulFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w) |
ClampedUIntAddFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w) |
ClampedUIntSubFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w) |
ClampedUIntMulFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w) |
IntSetWidthFn :: forall (m :: Natural) (n :: Natural) (f :: BaseType -> Type). (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType m) ('BaseBVType n) |
UIntSetWidthFn :: forall (m :: Natural) (n :: Natural) (f :: BaseType -> Type). (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType m) ('BaseBVType n) |
UIntToIntFn :: forall (m :: Natural) (n :: Natural) (f :: BaseType -> Type). (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType m) ('BaseBVType n) |
IntToUIntFn :: forall (m :: Natural) (n :: Natural) (f :: BaseType -> Type). (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType m) ('BaseBVType n) |
RealIsNonZeroFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseBoolType |
RealCosFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseRealType |
RealSinFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseRealType |
RealToSBVFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) ('BaseBVType w) |
RealToUBVFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) ('BaseBVType w) |
PredToBVFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBoolType) ('BaseBVType w) |
CplxIsNonZeroFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseBoolType |
CplxIsRealFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseBoolType |
RealToComplexFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseComplexType |
RealPartOfCplxFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseRealType |
ImagPartOfCplxFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseRealType |
CplxNegFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType |
CplxAddFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseComplexType) '::> BaseComplexType) 'BaseComplexType |
CplxSubFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseComplexType) '::> BaseComplexType) 'BaseComplexType |
CplxMulFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseComplexType) '::> BaseComplexType) 'BaseComplexType |
CplxRoundFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType |
CplxFloorFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType |
CplxCeilFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType |
CplxMagFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseRealType |
CplxSqrtFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType |
CplxExpFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType |
CplxLogFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType |
CplxLogBaseFn :: forall (f :: BaseType -> Type). !Integer -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType |
CplxSinFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType |
CplxCosFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType |
CplxTanFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType |

#### Instances

Instances details

TestEquality f => Eq (MatlabSolverFn f args tp) Source # |
Instance details Defined in What4.Expr.MATLAB Methods (==) :: MatlabSolverFn f args tp -> MatlabSolverFn f args tp -> Bool Source # (/=) :: MatlabSolverFn f args tp -> MatlabSolverFn f args tp -> Bool Source #
(Hashable (f BaseRealType), Hashable (f BaseIntegerType), HashableF f, TestEquality f) => Hashable (MatlabSolverFn f args tp) Source # |
Instance details Defined in What4.Expr.MATLAB Methods hashWithSalt :: Int -> MatlabSolverFn f args tp -> Int Source # hash :: MatlabSolverFn f args tp -> Int Source #

matlabSolverArgTypes :: forall (f :: BaseType -> Type) (args :: Ctx BaseType) (ret :: BaseType). MatlabSolverFn f args ret -> Assignment BaseTypeRepr args Source #

Get arg tpyes of solver fn.

matlabSolverReturnType :: forall (f :: BaseType -> Type) (args :: Ctx BaseType) (ret :: BaseType). MatlabSolverFn f args ret -> BaseTypeRepr ret Source #

Get return type of solver fn.

ppMatlabSolverFn :: forall (f :: BaseType -> Type) (a :: Ctx BaseType) (r :: BaseType) ann. IsExpr f => MatlabSolverFn f a r -> Doc ann Source #

evalMatlabSolverFn :: forall sym (args :: Ctx BaseType) (ret :: BaseType). IsExprBuilder sym => MatlabSolverFn (SymExpr sym) args ret -> sym -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret) Source #

testSolverFnEq :: forall (f :: BaseType -> Type) (ax :: Ctx BaseType) (rx :: BaseType) (ay :: Ctx BaseType) (ry :: BaseType). TestEquality f => MatlabSolverFn f ax rx -> MatlabSolverFn f ay ry -> Maybe ((ax ::> rx) :~: (ay ::> ry)) Source #

Test `MatlabSolverFn` values for equality.

traverseMatlabSolverFn :: forall m e f (a :: Ctx BaseType) (r :: BaseType). Applicative m => (forall (tp :: BaseType). e tp -> m (f tp)) -> MatlabSolverFn e a r -> m (MatlabSolverFn f a r) Source #

class IsSymExprBuilder sym => MatlabSymbolicArrayBuilder sym where Source #

This class is provides functions needed to implement the symbolic array intrinsic functions

Methods

mkMatlabSolverFn :: forall (args :: Ctx BaseType) (ret :: BaseType). sym -> MatlabSolverFn (SymExpr sym) args ret -> IO (SymFn sym args ret) Source #

Create a Matlab solver function from its prototype.

#### Instances

Instances details

MatlabSymbolicArrayBuilder (ExprBuilder t st fs) Source # |
Instance details Defined in What4.Expr.Builder Methods mkMatlabSolverFn :: forall (args :: Ctx BaseType) (ret :: BaseType). ExprBuilder t st fs -> MatlabSolverFn (SymExpr (ExprBuilder t st fs)) args ret -> IO (SymFn (ExprBuilder t st fs) args ret) Source #

# Utilities for definition

clampedIntAdd :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #

clampedIntSub :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #

clampedIntMul :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #

clampedIntNeg :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w) Source #

Compute the clamped negation of a signed bitvector.

The only difference between this operation and the usual 2's complement negation function is the handling of MIN_INT. The usual 2's complement negation sends MIN_INT to MIN_INT; however, the clamped version instead sends MIN_INT to MAX_INT.

clampedIntAbs :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w) Source #

Compute the clamped absolute value of a signed bitvector.

The only difference between this operation and the usual 2's complement operation is the handling of MIN_INT. The usual 2's complement absolute value function sends MIN_INT to MIN_INT; however, the clamped version instead sends MIN_INT to MAX_INT.

clampedUIntAdd :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #

clampedUIntSub :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #

clampedUIntMul :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #