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

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

What4.Expr.AppTheory

Description

Synopsis

- data AppTheory
  - = BoolTheory
  - | LinearArithTheory
  - | NonlinearArithTheory
  - | ComputableArithTheory
  - | BitvectorTheory
  - | QuantifierTheory
  - | StringTheory
  - | FloatingPointTheory
  - | ArrayTheory
  - | StructTheory
  - | FnTheory
- quantTheory :: NonceApp t (Expr t) tp -> AppTheory
- appTheory :: App (Expr t) tp -> AppTheory
- typeTheory :: BaseTypeRepr tp -> AppTheory

# Documentation

data AppTheory Source #

The theory that a symbol belongs to.

Constructors

BoolTheory |
LinearArithTheory |
NonlinearArithTheory |
ComputableArithTheory |
BitvectorTheory |
QuantifierTheory |
StringTheory |
FloatingPointTheory |
ArrayTheory |
StructTheory | Theory attributed to structs (equivalent to records in CVC4CVC5Z3, tuples in Yices)
FnTheory | Theory attributed application functions.

#### Instances

Instances details

Eq AppTheory Source # |
Instance details Defined in What4.Expr.AppTheory Methods (==) :: AppTheory -> AppTheory -> Bool Source # (/=) :: AppTheory -> AppTheory -> Bool Source #
Ord AppTheory Source # |

Instance details

Defined in What4.Expr.AppTheory

Methods

compare :: AppTheory -> AppTheory -> Ordering Source #

(<) :: AppTheory -> AppTheory -> Bool Source #

(<=) :: AppTheory -> AppTheory -> Bool Source #

(>) :: AppTheory -> AppTheory -> Bool Source #

(>=) :: AppTheory -> AppTheory -> Bool Source #

max :: AppTheory -> AppTheory -> AppTheory Source #

min :: AppTheory -> AppTheory -> AppTheory Source #

quantTheory :: NonceApp t (Expr t) tp -> AppTheory Source #

appTheory :: App (Expr t) tp -> AppTheory Source #

typeTheory :: BaseTypeRepr tp -> AppTheory Source #