what4-1.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2016-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

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

Documentation

data ProblemFeatures Source #

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

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.