------------------------------------------------------------------------
-- |
-- Module      : What4.Expr.AppTheory
-- Description : Identifying the solver theory required by a core expression
-- Copyright   : (c) Galois, Inc 2016-2020
-- License     : BSD3
-- Maintainer  : Joe Hendrix <jhendrix@galois.com>
-- Stability   : provisional
------------------------------------------------------------------------

{-# LANGUAGE GADTs #-}
module What4.Expr.AppTheory
  ( AppTheory(..)
  , quantTheory
  , appTheory
  , typeTheory
  ) where

import           What4.BaseTypes
import           What4.Expr.Builder
import qualified What4.SemiRing as SR
import qualified What4.Expr.WeightedSum as WSum

-- | The theory that a symbol belongs to.
data AppTheory
   = 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.
   deriving (AppTheory -> AppTheory -> Bool
(AppTheory -> AppTheory -> Bool)
-> (AppTheory -> AppTheory -> Bool) -> Eq AppTheory
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AppTheory -> AppTheory -> Bool
$c/= :: AppTheory -> AppTheory -> Bool
== :: AppTheory -> AppTheory -> Bool
$c== :: AppTheory -> AppTheory -> Bool
Eq, Eq AppTheory
Eq AppTheory
-> (AppTheory -> AppTheory -> Ordering)
-> (AppTheory -> AppTheory -> Bool)
-> (AppTheory -> AppTheory -> Bool)
-> (AppTheory -> AppTheory -> Bool)
-> (AppTheory -> AppTheory -> Bool)
-> (AppTheory -> AppTheory -> AppTheory)
-> (AppTheory -> AppTheory -> AppTheory)
-> Ord AppTheory
AppTheory -> AppTheory -> Bool
AppTheory -> AppTheory -> Ordering
AppTheory -> AppTheory -> AppTheory
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: AppTheory -> AppTheory -> AppTheory
$cmin :: AppTheory -> AppTheory -> AppTheory
max :: AppTheory -> AppTheory -> AppTheory
$cmax :: AppTheory -> AppTheory -> AppTheory
>= :: AppTheory -> AppTheory -> Bool
$c>= :: AppTheory -> AppTheory -> Bool
> :: AppTheory -> AppTheory -> Bool
$c> :: AppTheory -> AppTheory -> Bool
<= :: AppTheory -> AppTheory -> Bool
$c<= :: AppTheory -> AppTheory -> Bool
< :: AppTheory -> AppTheory -> Bool
$c< :: AppTheory -> AppTheory -> Bool
compare :: AppTheory -> AppTheory -> Ordering
$ccompare :: AppTheory -> AppTheory -> Ordering
$cp1Ord :: Eq AppTheory
Ord)

quantTheory :: NonceApp t (Expr t) tp -> AppTheory
quantTheory :: NonceApp t (Expr t) tp -> AppTheory
quantTheory NonceApp t (Expr t) tp
a0 =
  case NonceApp t (Expr t) tp
a0 of
    Annotation BaseTypeRepr tp
tpr Nonce t tp
_ Expr t tp
_ -> BaseTypeRepr tp -> AppTheory
forall (tp :: BaseType). BaseTypeRepr tp -> AppTheory
typeTheory BaseTypeRepr tp
tpr
    Forall{} -> AppTheory
QuantifierTheory
    Exists{} -> AppTheory
QuantifierTheory
    ArrayFromFn{}   -> AppTheory
FnTheory
    MapOverArrays{} -> AppTheory
ArrayTheory
    ArrayTrueOnEntries{} -> AppTheory
ArrayTheory
    FnApp{} -> AppTheory
FnTheory

typeTheory :: BaseTypeRepr tp -> AppTheory
typeTheory :: BaseTypeRepr tp -> AppTheory
typeTheory BaseTypeRepr tp
tp = case BaseTypeRepr tp
tp of
  BaseTypeRepr tp
BaseBoolRepr      -> AppTheory
BoolTheory
  BaseBVRepr NatRepr w
_      -> AppTheory
BitvectorTheory
  BaseTypeRepr tp
BaseIntegerRepr   -> AppTheory
LinearArithTheory
  BaseTypeRepr tp
BaseRealRepr      -> AppTheory
LinearArithTheory
  BaseFloatRepr FloatPrecisionRepr fpp
_   -> AppTheory
FloatingPointTheory
  BaseStringRepr{}  -> AppTheory
StringTheory
  BaseTypeRepr tp
BaseComplexRepr   -> AppTheory
LinearArithTheory
  BaseStructRepr Assignment BaseTypeRepr ctx
_  -> AppTheory
StructTheory
  BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_ BaseTypeRepr xs
_ -> AppTheory
ArrayTheory

appTheory :: App (Expr t) tp -> AppTheory
appTheory :: App (Expr t) tp -> AppTheory
appTheory App (Expr t) tp
a0 =
  case App (Expr t) tp
a0 of
    ----------------------------
    -- Boolean operations

    BaseIte BaseTypeRepr tp
tp Integer
_ Expr t BaseBoolType
_ Expr t tp
_ Expr t tp
_ -> BaseTypeRepr tp -> AppTheory
forall (tp :: BaseType). BaseTypeRepr tp -> AppTheory
typeTheory BaseTypeRepr tp
tp
    BaseEq BaseTypeRepr tp
tp Expr t tp
_ Expr t tp
_ -> BaseTypeRepr tp -> AppTheory
forall (tp :: BaseType). BaseTypeRepr tp -> AppTheory
typeTheory BaseTypeRepr tp
tp

    NotPred{} -> AppTheory
BoolTheory
    ConjPred{} -> AppTheory
BoolTheory

    RealIsInteger{} -> AppTheory
LinearArithTheory

    BVTestBit{} -> AppTheory
BitvectorTheory
    BVSlt{} -> AppTheory
BitvectorTheory
    BVUlt{} -> AppTheory
BitvectorTheory
    BVOrBits{} -> AppTheory
BitvectorTheory

    ----------------------------
    -- Semiring operations
    SemiRingProd SemiRingProduct (Expr t) sr
pd ->
      case SemiRingProduct (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> SemiRingRepr sr
WSum.prodRepr SemiRingProduct (Expr t) sr
pd of
        SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
_ -> AppTheory
BitvectorTheory
        SemiRingRepr sr
SR.SemiRingIntegerRepr -> AppTheory
NonlinearArithTheory
        SemiRingRepr sr
SR.SemiRingRealRepr -> AppTheory
NonlinearArithTheory

    SemiRingSum WeightedSum (Expr t) sr
sm ->
      case WeightedSum (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> SemiRingRepr sr
WSum.sumRepr WeightedSum (Expr t) sr
sm of
        SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
_ -> AppTheory
BitvectorTheory
        SemiRingRepr sr
SR.SemiRingIntegerRepr -> AppTheory
LinearArithTheory
        SemiRingRepr sr
SR.SemiRingRealRepr -> AppTheory
LinearArithTheory

    SemiRingLe{} -> AppTheory
LinearArithTheory

    ----------------------------
    -- Integer operations

    IntMod Expr t BaseIntegerType
_ SemiRingLiteral{} -> AppTheory
LinearArithTheory
    IntMod{} -> AppTheory
NonlinearArithTheory

    IntDiv Expr t BaseIntegerType
_ SemiRingLiteral{} -> AppTheory
LinearArithTheory
    IntDiv{} -> AppTheory
NonlinearArithTheory

    IntAbs{} -> AppTheory
LinearArithTheory
    IntDivisible{} -> AppTheory
LinearArithTheory

    ----------------------------
    -- Real operations

    RealDiv{} -> AppTheory
NonlinearArithTheory
    RealSqrt{} -> AppTheory
NonlinearArithTheory

    ----------------------------
    -- Computable number operations
    App (Expr t) tp
Pi -> AppTheory
ComputableArithTheory
    RealSin{}   -> AppTheory
ComputableArithTheory
    RealCos{}   -> AppTheory
ComputableArithTheory
    RealATan2{} -> AppTheory
ComputableArithTheory
    RealSinh{}  -> AppTheory
ComputableArithTheory
    RealCosh{}  -> AppTheory
ComputableArithTheory
    RealExp{}   -> AppTheory
ComputableArithTheory
    RealLog{}   -> AppTheory
ComputableArithTheory

    ----------------------------
    -- Bitvector operations
    BVUnaryTerm{} -> AppTheory
BoolTheory
    BVConcat{} -> AppTheory
BitvectorTheory
    BVSelect{} -> AppTheory
BitvectorTheory
    BVUdiv{} -> AppTheory
BitvectorTheory
    BVUrem{} -> AppTheory
BitvectorTheory
    BVSdiv{} -> AppTheory
BitvectorTheory
    BVSrem{} -> AppTheory
BitvectorTheory
    BVShl{}   -> AppTheory
BitvectorTheory
    BVLshr{}  -> AppTheory
BitvectorTheory
    BVRol{}   -> AppTheory
BitvectorTheory
    BVRor{}   -> AppTheory
BitvectorTheory
    BVAshr{}  -> AppTheory
BitvectorTheory
    BVZext{}  -> AppTheory
BitvectorTheory
    BVSext{}  -> AppTheory
BitvectorTheory
    BVPopcount{} -> AppTheory
BitvectorTheory
    BVCountLeadingZeros{} -> AppTheory
BitvectorTheory
    BVCountTrailingZeros{} -> AppTheory
BitvectorTheory
    BVFill{} -> AppTheory
BitvectorTheory

    ----------------------------
    -- Float operations

    FloatNeg{}        -> AppTheory
FloatingPointTheory
    FloatAbs{}        -> AppTheory
FloatingPointTheory
    FloatSqrt{}       -> AppTheory
FloatingPointTheory
    FloatAdd{}        -> AppTheory
FloatingPointTheory
    FloatSub{}        -> AppTheory
FloatingPointTheory
    FloatMul{}        -> AppTheory
FloatingPointTheory
    FloatDiv{}        -> AppTheory
FloatingPointTheory
    FloatRem{}        -> AppTheory
FloatingPointTheory
    FloatFMA{}        -> AppTheory
FloatingPointTheory
    FloatFpEq{}       -> AppTheory
FloatingPointTheory
    FloatLe{}         -> AppTheory
FloatingPointTheory
    FloatLt{}         -> AppTheory
FloatingPointTheory
    FloatIsNaN{}      -> AppTheory
FloatingPointTheory
    FloatIsInf{}      -> AppTheory
FloatingPointTheory
    FloatIsZero{}     -> AppTheory
FloatingPointTheory
    FloatIsPos{}      -> AppTheory
FloatingPointTheory
    FloatIsNeg{}      -> AppTheory
FloatingPointTheory
    FloatIsSubnorm{}  -> AppTheory
FloatingPointTheory
    FloatIsNorm{}     -> AppTheory
FloatingPointTheory
    FloatCast{}       -> AppTheory
FloatingPointTheory
    FloatRound{}      -> AppTheory
FloatingPointTheory
    FloatFromBinary{} -> AppTheory
FloatingPointTheory
    FloatToBinary{}   -> AppTheory
FloatingPointTheory
    BVToFloat{}       -> AppTheory
FloatingPointTheory
    SBVToFloat{}      -> AppTheory
FloatingPointTheory
    RealToFloat{}     -> AppTheory
FloatingPointTheory
    FloatToBV{}       -> AppTheory
FloatingPointTheory
    FloatToSBV{}      -> AppTheory
FloatingPointTheory
    FloatToReal{}     -> AppTheory
FloatingPointTheory

    --------------------------------
    -- Conversions.

    IntegerToReal{} -> AppTheory
LinearArithTheory
    BVToInteger{}   -> AppTheory
LinearArithTheory
    SBVToInteger{}  -> AppTheory
LinearArithTheory

    RoundReal{} -> AppTheory
LinearArithTheory
    RoundEvenReal{} -> AppTheory
LinearArithTheory
    FloorReal{} -> AppTheory
LinearArithTheory
    CeilReal{}  -> AppTheory
LinearArithTheory
    RealToInteger{} -> AppTheory
LinearArithTheory

    IntegerToBV{}  -> AppTheory
BitvectorTheory

    ---------------------
    -- Array operations

    ArrayMap{} -> AppTheory
ArrayTheory
    ConstantArray{} -> AppTheory
ArrayTheory
    SelectArray{} -> AppTheory
ArrayTheory
    UpdateArray{} -> AppTheory
ArrayTheory

    ---------------------
    -- String operations
    StringAppend{} -> AppTheory
StringTheory
    StringLength{} -> AppTheory
StringTheory
    StringContains{} -> AppTheory
StringTheory
    StringIndexOf{} -> AppTheory
StringTheory
    StringIsPrefixOf{} -> AppTheory
StringTheory
    StringIsSuffixOf{} -> AppTheory
StringTheory
    StringSubstring{} -> AppTheory
StringTheory

    ---------------------
    -- Complex operations

    Cplx{} -> AppTheory
LinearArithTheory
    RealPart{} -> AppTheory
LinearArithTheory
    ImagPart{} -> AppTheory
LinearArithTheory

    ---------------------
    -- Struct operations

    -- A struct with its fields.
    StructCtor{}  -> AppTheory
StructTheory
    StructField{} -> AppTheory
StructTheory