    ------------------------------------------------------------------------
    -- |
    -- Module      : What4.ProblemFeatures
    -- Description : Descriptions of the "features" that can occur in queries
    -- Copyright   : (c) Galois, Inc 2016-2020
    -- License     : BSD3
    -- Maintainer  : Joe Hendrix <jhendrix@galois.com>
    -- Stability   : provisional
    --
    -- ProblemFeatures uses bit mask to represent the features.  The bits are:
    --
    --  0 : Uses linear arithmetic
    --  1 : Uses non-linear arithmetic, i.e. multiplication (should also set bit 0)
    --  2 : Uses computational reals (should also set bits 0 & 1)
    --  3 : Uses integer variables (should also set bit 0)
    --  4 : Uses bitvectors
    --  5 : Uses exists-forall.
    --  6 : Uses quantifiers (should also set bit 5)
    --  7 : Uses symbolic arrays or complex numbers.
    --  8 : Uses structs
    --  9 : Uses strings
    -- 10 : Uses floating-point
    -- 11 : Computes UNSAT cores
    -- 12 : Computes UNSAT assumptions
    -- 13 : Uses uninterpreted functions
    -- 14 : Uses defined functions
    ------------------------------------------------------------------------

    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    module What4.ProblemFeatures
      ( ProblemFeatures
      , noFeatures
      , useLinearArithmetic
      , useNonlinearArithmetic
      , useComputableReals
      , useIntegerArithmetic
      , useBitvectors
      , useExistForall
      , useQuantifiers
      , useSymbolicArrays
      , useStructs
      , useStrings
      , useFloatingPoint
      , useUnsatCores
      , useUnsatAssumptions
      , useUninterpFunctions
      , useDefinedFunctions
      , useProduceAbducts
      , hasProblemFeature
      ) where

    import Data.Bits
    import Data.Word

    -- | Allowed features represents features that the constraint solver
    -- will need to support to solve the problem.
    newtype ProblemFeatures = ProblemFeatures Word64
      deriving (ProblemFeatures -> ProblemFeatures -> Bool
    (ProblemFeatures -> ProblemFeatures -> Bool)
    -> (ProblemFeatures -> ProblemFeatures -> Bool)
    -> Eq ProblemFeatures
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ProblemFeatures -> ProblemFeatures -> Bool
    == :: ProblemFeatures -> ProblemFeatures -> Bool
    $c/= :: ProblemFeatures -> ProblemFeatures -> Bool
    /= :: ProblemFeatures -> ProblemFeatures -> Bool
    Eq, Eq ProblemFeatures
    ProblemFeatures
    Eq ProblemFeatures =>
    (ProblemFeatures -> ProblemFeatures -> ProblemFeatures)
    -> (ProblemFeatures -> ProblemFeatures -> ProblemFeatures)
    -> (ProblemFeatures -> ProblemFeatures -> ProblemFeatures)
    -> (ProblemFeatures -> ProblemFeatures)
    -> (ProblemFeatures -> Int -> ProblemFeatures)
    -> (ProblemFeatures -> Int -> ProblemFeatures)
    -> ProblemFeatures
    -> (Int -> ProblemFeatures)
    -> (ProblemFeatures -> Int -> ProblemFeatures)
    -> (ProblemFeatures -> Int -> ProblemFeatures)
    -> (ProblemFeatures -> Int -> ProblemFeatures)
    -> (ProblemFeatures -> Int -> Bool)
    -> (ProblemFeatures -> Maybe Int)
    -> (ProblemFeatures -> Int)
    -> (ProblemFeatures -> Bool)
    -> (ProblemFeatures -> Int -> ProblemFeatures)
    -> (ProblemFeatures -> Int -> ProblemFeatures)
    -> (ProblemFeatures -> Int -> ProblemFeatures)
    -> (ProblemFeatures -> Int -> ProblemFeatures)
    -> (ProblemFeatures -> Int -> ProblemFeatures)
    -> (ProblemFeatures -> Int -> ProblemFeatures)
    -> (ProblemFeatures -> Int)
    -> Bits ProblemFeatures
    Int -> ProblemFeatures
    ProblemFeatures -> Bool
    ProblemFeatures -> Int
    ProblemFeatures -> Maybe Int
    ProblemFeatures -> ProblemFeatures
    ProblemFeatures -> Int -> Bool
    ProblemFeatures -> Int -> ProblemFeatures
    ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a.
    Eq a =>
    (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a)
    -> (a -> Int -> a)
    -> (a -> Int -> a)
    -> a
    -> (Int -> a)
    -> (a -> Int -> a)
    -> (a -> Int -> a)
    -> (a -> Int -> a)
    -> (a -> Int -> Bool)
    -> (a -> Maybe Int)
    -> (a -> Int)
    -> (a -> Bool)
    -> (a -> Int -> a)
    -> (a -> Int -> a)
    -> (a -> Int -> a)
    -> (a -> Int -> a)
    -> (a -> Int -> a)
    -> (a -> Int -> a)
    -> (a -> Int)
    -> Bits a
    $c.&. :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    .&. :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    $c.|. :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    .|. :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    $cxor :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    xor :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    $ccomplement :: ProblemFeatures -> ProblemFeatures
    complement :: ProblemFeatures -> ProblemFeatures
    $cshift :: ProblemFeatures -> Int -> ProblemFeatures
    shift :: ProblemFeatures -> Int -> ProblemFeatures
    $crotate :: ProblemFeatures -> Int -> ProblemFeatures
    rotate :: ProblemFeatures -> Int -> ProblemFeatures
    $czeroBits :: ProblemFeatures
    zeroBits :: ProblemFeatures
    $cbit :: Int -> ProblemFeatures
    bit :: Int -> ProblemFeatures
    $csetBit :: ProblemFeatures -> Int -> ProblemFeatures
    setBit :: ProblemFeatures -> Int -> ProblemFeatures
    $cclearBit :: ProblemFeatures -> Int -> ProblemFeatures
    clearBit :: ProblemFeatures -> Int -> ProblemFeatures
    $ccomplementBit :: ProblemFeatures -> Int -> ProblemFeatures
    complementBit :: ProblemFeatures -> Int -> ProblemFeatures
    $ctestBit :: ProblemFeatures -> Int -> Bool
    testBit :: ProblemFeatures -> Int -> Bool
    $cbitSizeMaybe :: ProblemFeatures -> Maybe Int
    bitSizeMaybe :: ProblemFeatures -> Maybe Int
    $cbitSize :: ProblemFeatures -> Int
    bitSize :: ProblemFeatures -> Int
    $cisSigned :: ProblemFeatures -> Bool
    isSigned :: ProblemFeatures -> Bool
    $cshiftL :: ProblemFeatures -> Int -> ProblemFeatures
    shiftL :: ProblemFeatures -> Int -> ProblemFeatures
    $cunsafeShiftL :: ProblemFeatures -> Int -> ProblemFeatures
    unsafeShiftL :: ProblemFeatures -> Int -> ProblemFeatures
    $cshiftR :: ProblemFeatures -> Int -> ProblemFeatures
    shiftR :: ProblemFeatures -> Int -> ProblemFeatures
    $cunsafeShiftR :: ProblemFeatures -> Int -> ProblemFeatures
    unsafeShiftR :: ProblemFeatures -> Int -> ProblemFeatures
    $crotateL :: ProblemFeatures -> Int -> ProblemFeatures
    rotateL :: ProblemFeatures -> Int -> ProblemFeatures
    $crotateR :: ProblemFeatures -> Int -> ProblemFeatures
    rotateR :: ProblemFeatures -> Int -> ProblemFeatures
    $cpopCount :: ProblemFeatures -> Int
    popCount :: ProblemFeatures -> Int
    Bits)

    noFeatures :: ProblemFeatures
    noFeatures :: ProblemFeatures
    noFeatures = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0

    -- | Indicates whether the problem uses linear arithmetic.
    useLinearArithmetic :: ProblemFeatures
    useLinearArithmetic :: ProblemFeatures
    useLinearArithmetic = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x01

    -- | Indicates whether the problem uses non-linear arithmetic.
    useNonlinearArithmetic :: ProblemFeatures
    useNonlinearArithmetic :: ProblemFeatures
    useNonlinearArithmetic = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x03

    -- | Indicates whether the problem uses computable real functions.
    useComputableReals :: ProblemFeatures
    useComputableReals :: ProblemFeatures
    useComputableReals = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x04 ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useNonlinearArithmetic

    -- | Indicates the problem contains integer variables.
    useIntegerArithmetic :: ProblemFeatures
    useIntegerArithmetic :: ProblemFeatures
    useIntegerArithmetic = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x08 ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useLinearArithmetic

    -- | Indicates whether the problem uses bitvectors.
    useBitvectors :: ProblemFeatures
    useBitvectors :: ProblemFeatures
    useBitvectors = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x10

    -- | Indicates whether the problem needs exists-forall support.
    useExistForall :: ProblemFeatures
    useExistForall :: ProblemFeatures
    useExistForall = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x20

    -- | Has general quantifier support.
    useQuantifiers :: ProblemFeatures
    useQuantifiers :: ProblemFeatures
    useQuantifiers = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x40 ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useExistForall

    -- | Indicates whether the problem uses symbolic arrays.
    useSymbolicArrays :: ProblemFeatures
    useSymbolicArrays :: ProblemFeatures
    useSymbolicArrays = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x80

    -- | Indicates whether the problem uses structs
    --
    -- Structs are modeled using constructors in CVC4/CVC5/Z3, and tuples
    -- in Yices.
    useStructs :: ProblemFeatures
    useStructs :: ProblemFeatures
    useStructs = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x100

    -- | Indicates whether the problem uses strings
    --
    --   Strings have some symbolic support in CVC4, CVC5, and Z3.
    useStrings :: ProblemFeatures
    useStrings :: ProblemFeatures
    useStrings = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x200

    -- | Indicates whether the problem uses floating-point
    --
    --   Floating-point has some symbolic support in CVC4, CVC5, and Z3.
    useFloatingPoint :: ProblemFeatures
    useFloatingPoint :: ProblemFeatures
    useFloatingPoint = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x400

    -- | Indicates if the solver is able and configured to compute UNSAT
    --   cores.
    useUnsatCores :: ProblemFeatures
    useUnsatCores :: ProblemFeatures
    useUnsatCores = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x800

    -- | Indicates if the solver is able and configured to compute UNSAT
    --   assumptions.
    useUnsatAssumptions :: ProblemFeatures
    useUnsatAssumptions :: ProblemFeatures
    useUnsatAssumptions = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x1000

    -- | Indicates if the solver is able and configured to use
    --   uninterpreted functions.
    useUninterpFunctions :: ProblemFeatures
    useUninterpFunctions :: ProblemFeatures
    useUninterpFunctions = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x2000

    -- | Indicates if the solver is able and configured to use
    --   defined functions.
    useDefinedFunctions :: ProblemFeatures
    useDefinedFunctions :: ProblemFeatures
    useDefinedFunctions = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x4000

    -- | Indicates if the solver is able and configured to
    --   produce abducts.
    useProduceAbducts :: ProblemFeatures
    useProduceAbducts :: ProblemFeatures
    useProduceAbducts = Word64 -> ProblemFeatures
    ProblemFeatures Word64
    0x8000

    -- | Tests if one set of problem features subsumes another.
    --   In particular, @hasProblemFeature x y@ is true iff
    --   the set of features in @x@ is a superset of those in @y@.
    hasProblemFeature :: ProblemFeatures -> ProblemFeatures -> Bool
    hasProblemFeature :: ProblemFeatures -> ProblemFeatures -> Bool
    hasProblemFeature ProblemFeatures
    x ProblemFeatures
    y = (ProblemFeatures
    x ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .&. ProblemFeatures
    y) ProblemFeatures -> ProblemFeatures -> Bool
    forall a. Eq a => a -> a -> Bool
    == ProblemFeatures
    y