content: ------------------------------------------------------------------------
  -- |
  -- 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 (Eq, Bits)
  
  noFeatures :: ProblemFeatures
  noFeatures = ProblemFeatures 0
  
  -- | Indicates whether the problem uses linear arithmetic.
  useLinearArithmetic :: ProblemFeatures
  useLinearArithmetic = ProblemFeatures 0x01
  
  -- | Indicates whether the problem uses non-linear arithmetic.
  useNonlinearArithmetic :: ProblemFeatures
  useNonlinearArithmetic = ProblemFeatures 0x03
  
  -- | Indicates whether the problem uses computable real functions.
  useComputableReals :: ProblemFeatures
  useComputableReals = ProblemFeatures 0x04 .|. useNonlinearArithmetic
  
  -- | Indicates the problem contains integer variables.
  useIntegerArithmetic :: ProblemFeatures
  useIntegerArithmetic = ProblemFeatures 0x08 .|. useLinearArithmetic
  
  -- | Indicates whether the problem uses bitvectors.
  useBitvectors :: ProblemFeatures
  useBitvectors = ProblemFeatures 0x10
  
  -- | Indicates whether the problem needs exists-forall support.
  useExistForall :: ProblemFeatures
  useExistForall = ProblemFeatures 0x20
  
  -- | Has general quantifier support.
  useQuantifiers :: ProblemFeatures
  useQuantifiers = ProblemFeatures 0x40 .|. useExistForall
  
  -- | Indicates whether the problem uses symbolic arrays.
  useSymbolicArrays :: ProblemFeatures
  useSymbolicArrays = ProblemFeatures 0x80
  
  -- | Indicates whether the problem uses structs
  --
  -- Structs are modeled using constructors in CVC4/CVC5/Z3, and tuples
  -- in Yices.
  useStructs :: ProblemFeatures
  useStructs = ProblemFeatures 0x100
  
  -- | Indicates whether the problem uses strings
  --
  --   Strings have some symbolic support in CVC4, CVC5, and Z3.
  useStrings :: ProblemFeatures
  useStrings = ProblemFeatures 0x200
  
  -- | Indicates whether the problem uses floating-point
  --
  --   Floating-point has some symbolic support in CVC4, CVC5, and Z3.
  useFloatingPoint :: ProblemFeatures
  useFloatingPoint = ProblemFeatures 0x400
  
  -- | Indicates if the solver is able and configured to compute UNSAT
  --   cores.
  useUnsatCores :: ProblemFeatures
  useUnsatCores = ProblemFeatures 0x800
  
  -- | Indicates if the solver is able and configured to compute UNSAT
  --   assumptions.
  useUnsatAssumptions :: ProblemFeatures
  useUnsatAssumptions = ProblemFeatures 0x1000
  
  -- | Indicates if the solver is able and configured to use
  --   uninterpreted functions.
  useUninterpFunctions :: ProblemFeatures
  useUninterpFunctions = ProblemFeatures 0x2000
  
  -- | Indicates if the solver is able and configured to use
  --   defined functions.
  useDefinedFunctions :: ProblemFeatures
  useDefinedFunctions = ProblemFeatures 0x4000
  
  -- | Indicates if the solver is able and configured to 
  --   produce abducts.
  useProduceAbducts :: ProblemFeatures
  useProduceAbducts = ProblemFeatures 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 x y = (x .&. y) == y
  