What4.ProblemFeatures

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

Documentation

data ProblemFeatures

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

Instances

Eq ProblemFeatures

Defined in What4.ProblemFeatures

Methods

(==) :: ProblemFeatures -> ProblemFeatures -> Bool

(/=) :: ProblemFeatures -> ProblemFeatures -> Bool

Bits ProblemFeatures

Defined in What4.ProblemFeatures

Methods

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

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

xor :: ProblemFeatures -> ProblemFeatures -> ProblemFeatures

complement :: ProblemFeatures -> ProblemFeatures

shift :: ProblemFeatures -> Int -> ProblemFeatures

rotate :: ProblemFeatures -> Int -> ProblemFeatures

zeroBits :: ProblemFeatures

bit :: Int -> ProblemFeatures

setBit :: ProblemFeatures -> Int -> ProblemFeatures

clearBit :: ProblemFeatures -> Int -> ProblemFeatures

complementBit :: ProblemFeatures -> Int -> ProblemFeatures

testBit :: ProblemFeatures -> Int -> Bool

bitSizeMaybe :: ProblemFeatures -> Maybe Int

bitSize :: ProblemFeatures -> Int

isSigned :: ProblemFeatures -> Bool

shiftL :: ProblemFeatures -> Int -> ProblemFeatures

unsafeShiftL :: ProblemFeatures -> Int -> ProblemFeatures

shiftR :: ProblemFeatures -> Int -> ProblemFeatures

unsafeShiftR :: ProblemFeatures -> Int -> ProblemFeatures

rotateL :: ProblemFeatures -> Int -> ProblemFeatures

rotateR :: ProblemFeatures -> Int -> ProblemFeatures

popCount :: ProblemFeatures -> Int

noFeatures :: ProblemFeatures

useLinearArithmetic :: ProblemFeatures

Indicates whether the problem uses linear arithmetic.

useNonlinearArithmetic :: ProblemFeatures

Indicates whether the problem uses non-linear arithmetic.

useComputableReals :: ProblemFeatures

Indicates whether the problem uses computable real functions.

useIntegerArithmetic :: ProblemFeatures

Indicates the problem contains integer variables.

useBitvectors :: ProblemFeatures

Indicates whether the problem uses bitvectors.

useExistForall :: ProblemFeatures

Indicates whether the problem needs exists-forall support.

useQuantifiers :: ProblemFeatures

Has general quantifier support.

useSymbolicArrays :: ProblemFeatures

Indicates whether the problem uses symbolic arrays.

useStructs :: ProblemFeatures

Indicates whether the problem uses structs

Structs are modeled using constructors in CVC4/Z3, and tuples in Yices.

useStrings :: ProblemFeatures

Indicates whether the problem uses strings

Strings have some symbolic support in CVC4 and Z3.

useFloatingPoint :: ProblemFeatures

Indicates whether the problem uses floating-point

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

useUnsatCores :: ProblemFeatures

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

useUnsatAssumptions :: ProblemFeatures

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

hasProblemFeature :: ProblemFeatures -> ProblemFeatures -> Bool