- data E a
- data V a
- class AllE a where
- class AllE a => NumE a
- type Name = String
- true :: E Bool
- false :: E Bool
- constant :: AllE a => a -> E a
- ref :: AllE a => V a -> E a
- not_ :: E Bool -> E Bool
- (&&.) :: E Bool -> E Bool -> E Bool
- (||.) :: E Bool -> E Bool -> E Bool
- and_ :: [E Bool] -> E Bool
- or_ :: [E Bool] -> E Bool
- any_ :: (a -> E Bool) -> [a] -> E Bool
- all_ :: (a -> E Bool) -> [a] -> E Bool
- imply :: E Bool -> E Bool -> E Bool
- (==.) :: AllE a => E a -> E a -> E Bool
- (/=.) :: AllE a => E a -> E a -> E Bool
- (<.) :: NumE a => E a -> E a -> E Bool
- (<=.) :: NumE a => E a -> E a -> E Bool
- (>.) :: NumE a => E a -> E a -> E Bool
- (>=.) :: NumE a => E a -> E a -> E Bool
- min_ :: NumE a => E a -> E a -> E a
- minimum_ :: NumE a => [E a] -> E a
- max_ :: NumE a => E a -> E a -> E a
- maximum_ :: NumE a => [E a] -> E a
- limit :: NumE a => E a -> E a -> E a -> E a
- (*.) :: NumE a => E a -> a -> E a
- (/.) :: E Float -> Float -> E Float
- div_ :: E Int -> Int -> E Int
- mod_ :: E Int -> Int -> E Int
- mux :: AllE a => E Bool -> E a -> E a -> E a
- linear :: (Float, Float) -> (Float, Float) -> E Float -> E Float
- data Stmt a
- scope :: Name -> Stmt a -> Stmt a
- annotate :: Name -> Stmt a -> Stmt a
- bool :: Name -> Bool -> Stmt (V Bool)
- bool' :: Name -> E Bool -> Stmt (E Bool)
- int :: Name -> Int -> Stmt (V Int)
- int' :: Name -> E Int -> Stmt (E Int)
- float :: Name -> Float -> Stmt (V Float)
- float' :: Name -> E Float -> Stmt (E Float)
- input :: AllE a => (Name -> a -> Stmt (V a)) -> Name -> Stmt (E a)
- (<==) :: Assign a => V a -> E a -> Stmt ()
- ifelse :: Name -> E Bool -> Stmt () -> Stmt () -> Stmt ()
- if_ :: Name -> E Bool -> Stmt () -> Stmt ()
- incr :: V Int -> Stmt ()
- decr :: V Int -> Stmt ()
- assert :: Name -> E Bool -> Stmt ()
- assume :: Name -> E Bool -> Stmt ()
- verify :: FilePath -> Int -> Stmt () -> IO ()
- code :: Name -> Stmt () -> IO ()
Types
Expressions
Constants
Variable Reference
Logical Operations
Equality and Comparison
Min, Max, and Limiting
Arithmetic Operations
Conditional Operator
Lookups
linear :: (Float, Float) -> (Float, Float) -> E Float -> E FloatSource
Linear interpolation and extrapolation between two points.
Statements
Hierarchical Scope and Annotations
annotate :: Name -> Stmt a -> Stmt aSource
Add an annotation to a statement. Useful for requirement trace tags.
Variable Declarations
bool' :: Name -> E Bool -> Stmt (E Bool)Source
Boolean variable declaration and immediate assignment.
float' :: Name -> E Float -> Stmt (E Float)Source
Float variable declaration and immediate assignment.
input :: AllE a => (Name -> a -> Stmt (V a)) -> Name -> Stmt (E a)Source
Input variable declaration. Input variables are initialized to 0.
Variable Assignment
Conditional Execution
Incrementing and decrementing.
Assertions and Assumptions
Verification
verify :: FilePath -> Int -> Stmt () -> IO ()Source
Verify a program.
^ verify pathToYices maxK program