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

Copyright | (c) Galois Inc 2016-2020
License | BSD3
Maintainer | Joe Hendrix <jhendrix@galois.com>
Stability | provisional
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.ProblemFeatures

Description

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

Synopsis

- data ProblemFeatures
- noFeatures :: ProblemFeatures
- useLinearArithmetic :: ProblemFeatures
- useNonlinearArithmetic :: ProblemFeatures
- useComputableReals :: ProblemFeatures
- useIntegerArithmetic :: ProblemFeatures
- useBitvectors :: ProblemFeatures
- useExistForall :: ProblemFeatures
- useQuantifiers :: ProblemFeatures
- useSymbolicArrays :: ProblemFeatures
- useStructs :: ProblemFeatures
- useStrings :: ProblemFeatures
- useFloatingPoint :: ProblemFeatures
- useUnsatCores :: ProblemFeatures
- useUnsatAssumptions :: ProblemFeatures
- useUninterpFunctions :: ProblemFeatures
- useDefinedFunctions :: ProblemFeatures
- useProduceAbducts :: ProblemFeatures
- hasProblemFeature :: ProblemFeatures -> ProblemFeatures -> Bool

# Documentation

data ProblemFeatures Source #

Allowed features represents features that the constraint solver will need to support to solve the problem.

#### Instances

Instances details

Bits ProblemFeatures Source # |

Instance details

Defined in What4.ProblemFeatures

Methods

(.&.) :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures Source #

(.|.) :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures Source #

xor :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures Source #

complement :: ProblemFeatures -> ProblemFeatures Source #

shift :: ProblemFeatures -> Int -> ProblemFeatures Source #

rotate :: ProblemFeatures -> Int -> ProblemFeatures Source #

zeroBits :: ProblemFeatures Source #

bit :: Int -> ProblemFeatures Source #

setBit :: ProblemFeatures -> Int -> ProblemFeatures Source #

clearBit :: ProblemFeatures -> Int -> ProblemFeatures Source #

complementBit :: ProblemFeatures -> Int -> ProblemFeatures Source #

testBit :: ProblemFeatures -> Int -> Bool Source #

bitSizeMaybe :: ProblemFeatures -> Maybe Int Source #

bitSize :: ProblemFeatures -> Int Source #

isSigned :: ProblemFeatures -> Bool Source #

shiftL :: ProblemFeatures -> Int -> ProblemFeatures Source #

unsafeShiftL :: ProblemFeatures -> Int -> ProblemFeatures Source #

shiftR :: ProblemFeatures -> Int -> ProblemFeatures Source #

unsafeShiftR :: ProblemFeatures -> Int -> ProblemFeatures Source #

rotateL :: ProblemFeatures -> Int -> ProblemFeatures Source #

rotateR :: ProblemFeatures -> Int -> ProblemFeatures Source #

popCount :: ProblemFeatures -> Int Source #

Eq ProblemFeatures Source # |
Instance details Defined in What4.ProblemFeatures Methods (==) :: ProblemFeatures -> ProblemFeatures -> Bool Source # (/=) :: ProblemFeatures -> ProblemFeatures -> Bool Source #

noFeatures :: ProblemFeatures Source #

useLinearArithmetic :: ProblemFeatures Source #

Indicates whether the problem uses linear arithmetic.

useNonlinearArithmetic :: ProblemFeatures Source #

Indicates whether the problem uses non-linear arithmetic.

useComputableReals :: ProblemFeatures Source #

Indicates whether the problem uses computable real functions.

useIntegerArithmetic :: ProblemFeatures Source #

Indicates the problem contains integer variables.

useBitvectors :: ProblemFeatures Source #

Indicates whether the problem uses bitvectors.

useExistForall :: ProblemFeatures Source #

Indicates whether the problem needs exists-forall support.

useQuantifiers :: ProblemFeatures Source #

Has general quantifier support.

useSymbolicArrays :: ProblemFeatures Source #

Indicates whether the problem uses symbolic arrays.

useStructs :: ProblemFeatures Source #

Indicates whether the problem uses structs

Structs are modeled using constructors in CVC4CVC5Z3, and tuples in Yices.

useStrings :: ProblemFeatures Source #

Indicates whether the problem uses strings

Strings have some symbolic support in CVC4, CVC5, and Z3.

useFloatingPoint :: ProblemFeatures Source #

Indicates whether the problem uses floating-point

Floating-point has some symbolic support in CVC4, CVC5, and Z3.

useUnsatCores :: ProblemFeatures Source #

Indicates if the solver is able and configured to compute UNSAT cores.

useUnsatAssumptions :: ProblemFeatures Source #

Indicates if the solver is able and configured to compute UNSAT assumptions.

useUninterpFunctions :: ProblemFeatures Source #

Indicates if the solver is able and configured to use uninterpreted functions.

useDefinedFunctions :: ProblemFeatures Source #

Indicates if the solver is able and configured to use defined functions.

useProduceAbducts :: ProblemFeatures Source #

Indicates if the solver is able and configured to produce abducts.

hasProblemFeature :: ProblemFeatures -> ProblemFeatures -> Bool Source #

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