| Copyright | (c) Galois Inc 2016-2020 |
|---|---|
| License | BSD3 |
| Maintainer | Joe Hendrix <jhendrix@galois.com> |
| Stability | provisional |
| Safe Haskell | None |
| 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
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
- 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
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 CVC4/Z3, and tuples in Yices.
useStrings :: ProblemFeatures Source #
Indicates whether the problem uses strings
Strings have some symbolic support in CVC4 and Z3.
useFloatingPoint :: ProblemFeatures Source #
Indicates whether the problem uses floating-point
Floating-point has some symbolic support in CVC4 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.