Copyright | (c) Galois Inc 2016-2020 |
---|---|

License | BSD3 |

Maintainer | Joe Hendrix <jhendrix@galois.com> |

Stability | provisional |

Safe Haskell | None |

Language | Haskell2010 |

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.