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

Copyright(c) Galois Inc 2016-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Stabilityprovisional
Safe HaskellNone
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 CVC4/Z3, tuples in Yices)

FnTheory

Theory attributed application functions.