------------------------------------------------------------------------
-- |
-- 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
------------------------------------------------------------------------

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module What4.ProblemFeatures
  ( ProblemFeatures
  , noFeatures
  , useLinearArithmetic
  , useNonlinearArithmetic
  , useComputableReals
  , useIntegerArithmetic
  , useBitvectors
  , useExistForall
  , useQuantifiers
  , useSymbolicArrays
  , useStructs
  , useStrings
  , useFloatingPoint
  , useUnsatCores
  , useUnsatAssumptions
  , 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
/= :: ProblemFeatures -> ProblemFeatures -> Bool
$c/= :: ProblemFeatures -> ProblemFeatures -> Bool
== :: ProblemFeatures -> ProblemFeatures -> Bool
$c== :: 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
popCount :: ProblemFeatures -> Int
$cpopCount :: ProblemFeatures -> Int
rotateR :: ProblemFeatures -> Int -> ProblemFeatures
$crotateR :: ProblemFeatures -> Int -> ProblemFeatures
rotateL :: ProblemFeatures -> Int -> ProblemFeatures
$crotateL :: ProblemFeatures -> Int -> ProblemFeatures
unsafeShiftR :: ProblemFeatures -> Int -> ProblemFeatures
$cunsafeShiftR :: ProblemFeatures -> Int -> ProblemFeatures
shiftR :: ProblemFeatures -> Int -> ProblemFeatures
$cshiftR :: ProblemFeatures -> Int -> ProblemFeatures
unsafeShiftL :: ProblemFeatures -> Int -> ProblemFeatures
$cunsafeShiftL :: ProblemFeatures -> Int -> ProblemFeatures
shiftL :: ProblemFeatures -> Int -> ProblemFeatures
$cshiftL :: ProblemFeatures -> Int -> ProblemFeatures
isSigned :: ProblemFeatures -> Bool
$cisSigned :: ProblemFeatures -> Bool
bitSize :: ProblemFeatures -> Int
$cbitSize :: ProblemFeatures -> Int
bitSizeMaybe :: ProblemFeatures -> Maybe Int
$cbitSizeMaybe :: ProblemFeatures -> Maybe Int
testBit :: ProblemFeatures -> Int -> Bool
$ctestBit :: ProblemFeatures -> Int -> Bool
complementBit :: ProblemFeatures -> Int -> ProblemFeatures
$ccomplementBit :: ProblemFeatures -> Int -> ProblemFeatures
clearBit :: ProblemFeatures -> Int -> ProblemFeatures
$cclearBit :: ProblemFeatures -> Int -> ProblemFeatures
setBit :: ProblemFeatures -> Int -> ProblemFeatures
$csetBit :: ProblemFeatures -> Int -> ProblemFeatures
bit :: Int -> ProblemFeatures
$cbit :: Int -> ProblemFeatures
zeroBits :: ProblemFeatures
$czeroBits :: ProblemFeatures
rotate :: ProblemFeatures -> Int -> ProblemFeatures
$crotate :: ProblemFeatures -> Int -> ProblemFeatures
shift :: ProblemFeatures -> Int -> ProblemFeatures
$cshift :: ProblemFeatures -> Int -> ProblemFeatures
complement :: ProblemFeatures -> ProblemFeatures
$ccomplement :: ProblemFeatures -> ProblemFeatures
xor :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures
$cxor :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures
.|. :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures
$c.|. :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures
.&. :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures
$c.&. :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures
$cp1Bits :: Eq ProblemFeatures
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/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 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 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

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