what4-1.5.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2016-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Stabilityprovisional
Safe HaskellSafe-Inferred
LanguageHaskell2010

What4.Expr.AppTheory

Description

 
Synopsis

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 #

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

Ord AppTheory Source # 
Instance details

Defined in What4.Expr.AppTheory

Methods

compare :: AppTheory -> AppTheory -> Ordering #

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

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

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

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

max :: AppTheory -> AppTheory -> AppTheory #

min :: AppTheory -> AppTheory -> AppTheory #

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

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

typeTheory :: BaseTypeRepr tp -> AppTheory Source #