what4-1.6.3: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2014-2020
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

What4.Protocol.SMTLib2

Description

This module defines operations for producing SMTLib2-compatible queries useful for interfacing with solvers that accecpt SMTLib2 as an input language.

Synopsis

Documentation

data Writer a Source #

Instances

Instances details
OnlineSolver (Writer Bitwuzla) Source # 
Instance details

Defined in What4.Solver.Bitwuzla

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Bitwuzla)) Source #

shutdownSolverProcess :: SolverProcess scope (Writer Bitwuzla) -> IO (ExitCode, Text) Source #

OnlineSolver (Writer Boolector) Source # 
Instance details

Defined in What4.Solver.Boolector

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Boolector)) Source #

shutdownSolverProcess :: SolverProcess scope (Writer Boolector) -> IO (ExitCode, Text) Source #

OnlineSolver (Writer CVC4) Source # 
Instance details

Defined in What4.Solver.CVC4

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer CVC4)) Source #

shutdownSolverProcess :: SolverProcess scope (Writer CVC4) -> IO (ExitCode, Text) Source #

OnlineSolver (Writer CVC5) Source # 
Instance details

Defined in What4.Solver.CVC5

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer CVC5)) Source #

shutdownSolverProcess :: SolverProcess scope (Writer CVC5) -> IO (ExitCode, Text) Source #

OnlineSolver (Writer STP) Source # 
Instance details

Defined in What4.Solver.STP

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer STP)) Source #

shutdownSolverProcess :: SolverProcess scope (Writer STP) -> IO (ExitCode, Text) Source #

OnlineSolver (Writer Z3) Source # 
Instance details

Defined in What4.Solver.Z3

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Z3)) Source #

shutdownSolverProcess :: SolverProcess scope (Writer Z3) -> IO (ExitCode, Text) Source #

SMTLib2Tweaks a => SMTReadWriter (Writer a) Source # 
Instance details

Defined in What4.Protocol.SMTLib2

Methods

smtEvalFuns :: WriterConn t (Writer a) -> InputStream Text -> SMTEvalFunctions (Writer a) Source #

smtSatResult :: f (Writer a) -> WriterConn t (Writer a) -> IO (SatResult () ()) Source #

smtUnsatCoreResult :: f (Writer a) -> WriterConn t (Writer a) -> IO [Text] Source #

smtAbductResult :: f (Writer a) -> WriterConn t (Writer a) -> Text -> Term (Writer a) -> IO String Source #

smtAbductNextResult :: f (Writer a) -> WriterConn t (Writer a) -> IO String Source #

smtUnsatAssumptionsResult :: f (Writer a) -> WriterConn t (Writer a) -> IO [(Bool, Text)] Source #

SMTLib2Tweaks a => SMTWriter (Writer a) Source # 
Instance details

Defined in What4.Protocol.SMTLib2

Methods

forallExpr :: [(Text, Some TypeMap)] -> Term (Writer a) -> Term (Writer a) Source #

existsExpr :: [(Text, Some TypeMap)] -> Term (Writer a) -> Term (Writer a) Source #

arrayConstant :: Maybe (ArrayConstantFn (Term (Writer a))) Source #

arraySelect :: Term (Writer a) -> [Term (Writer a)] -> Term (Writer a) Source #

arrayUpdate :: Term (Writer a) -> [Term (Writer a)] -> Term (Writer a) -> Term (Writer a) Source #

commentCommand :: f (Writer a) -> Builder -> Command (Writer a) Source #

assertCommand :: f (Writer a) -> Term (Writer a) -> Command (Writer a) Source #

assertNamedCommand :: f (Writer a) -> Term (Writer a) -> Text -> Command (Writer a) Source #

pushCommand :: f (Writer a) -> Command (Writer a) Source #

popCommand :: f (Writer a) -> Command (Writer a) Source #

push2Command :: f (Writer a) -> Command (Writer a) Source #

pop2Command :: f (Writer a) -> Command (Writer a) Source #

popManyCommands :: f (Writer a) -> Int -> [Command (Writer a)] Source #

resetCommand :: f (Writer a) -> Command (Writer a) Source #

checkCommands :: f (Writer a) -> [Command (Writer a)] Source #

checkWithAssumptionsCommands :: f (Writer a) -> [Text] -> [Command (Writer a)] Source #

getUnsatAssumptionsCommand :: f (Writer a) -> Command (Writer a) Source #

getUnsatCoreCommand :: f (Writer a) -> Command (Writer a) Source #

getAbductCommand :: f (Writer a) -> Text -> Term (Writer a) -> Command (Writer a) Source #

getAbductNextCommand :: f (Writer a) -> Command (Writer a) Source #

setOptCommand :: f (Writer a) -> Text -> Text -> Command (Writer a) Source #

declareCommand :: forall f (args :: Ctx BaseType) (rtp :: BaseType). f (Writer a) -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command (Writer a) Source #

defineCommand :: forall f (rtp :: BaseType). f (Writer a) -> Text -> [(Text, Some TypeMap)] -> TypeMap rtp -> Term (Writer a) -> Command (Writer a) Source #

synthFunCommand :: forall f (tp :: BaseType). f (Writer a) -> Text -> [(Text, Some TypeMap)] -> TypeMap tp -> Command (Writer a) Source #

declareVarCommand :: forall f (tp :: BaseType). f (Writer a) -> Text -> TypeMap tp -> Command (Writer a) Source #

constraintCommand :: f (Writer a) -> Term (Writer a) -> Command (Writer a) Source #

declareStructDatatype :: forall t (args :: Ctx BaseType). WriterConn t (Writer a) -> Assignment TypeMap args -> IO () Source #

structCtor :: forall (args :: Ctx BaseType). Assignment TypeMap args -> [Term (Writer a)] -> Term (Writer a) Source #

structProj :: forall (args :: Ctx BaseType) (tp :: BaseType). Assignment TypeMap args -> Index args tp -> Term (Writer a) -> Term (Writer a) Source #

stringTerm :: Text -> Term (Writer a) Source #

stringLength :: Term (Writer a) -> Term (Writer a) Source #

stringIndexOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringContains :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringIsPrefixOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringIsSuffixOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringSubstring :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringAppend :: [Term (Writer a)] -> Term (Writer a) Source #

resetDeclaredStructs :: WriterConn t (Writer a) -> IO () Source #

writeCommand :: WriterConn t (Writer a) -> Command (Writer a) -> IO () Source #

type Command (Writer a) Source # 
Instance details

Defined in What4.Protocol.SMTLib2

type Term (Writer a) Source # 
Instance details

Defined in What4.Protocol.SMTLib2

type Term (Writer a) = Term

class Show a => SMTLib2Tweaks a where Source #

This class exists so that solvers supporting the SMTLib2 format can support features that go slightly beyond the standard.

In particular, there is no standardized syntax for constant arrays (arrays which map every index to the same value). Solvers that support the theory of arrays and have custom syntax for constant arrays should implement smtlib2arrayConstant. In addition, solvers may override the default representation of complex numbers if necessary. The default is to represent complex numbers as "(Array Bool Real)" and to build instances by updating a constant array.

Minimal complete definition

smtlib2tweaks

Methods

smtlib2tweaks :: a Source #

smtlib2exitCommand :: Maybe Command Source #

smtlib2arrayType :: [Sort] -> Sort -> Sort Source #

Return a representation of the type associated with a (multi-dimensional) symbolic array.

By default, we encode symbolic arrays using a nested representation. If the solver, supports tuples/structs it may wish to change this.

smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term) Source #

smtlib2arraySelect :: Term -> [Term] -> Term Source #

smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term Source #

smtlib2StringSort :: Sort Source #

smtlib2StringTerm :: Text -> Term Source #

smtlib2StringLength :: Term -> Term Source #

smtlib2StringAppend :: [Term] -> Term Source #

smtlib2StringContains :: Term -> Term -> Term Source #

smtlib2StringIndexOf :: Term -> Term -> Term -> Term Source #

smtlib2StringIsPrefixOf :: Term -> Term -> Term Source #

smtlib2StringIsSuffixOf :: Term -> Term -> Term Source #

smtlib2StringSubstring :: Term -> Term -> Term -> Term Source #

smtlib2StructSort :: [Sort] -> Sort Source #

The sort of structs with the given field types.

By default, this uses SMTLIB2 datatypes and are not primitive to the language.

smtlib2StructCtor :: [Term] -> Term Source #

Construct a struct value from the given field values

smtlib2StructProj Source #

Arguments

:: Int

number of fields in the struct

-> Int

0-based index of the struct field

-> Term

struct term to project from

-> Term 

Construct a struct field projection term

smtlib2declareStructCmd :: Int -> Maybe Command Source #

Instances

Instances details
SMTLib2Tweaks Bitwuzla Source # 
Instance details

Defined in What4.Solver.Bitwuzla

SMTLib2Tweaks Boolector Source # 
Instance details

Defined in What4.Solver.Boolector

SMTLib2Tweaks CVC4 Source # 
Instance details

Defined in What4.Solver.CVC4

SMTLib2Tweaks CVC5 Source # 
Instance details

Defined in What4.Solver.CVC5

SMTLib2Tweaks DReal Source # 
Instance details

Defined in What4.Solver.DReal

SMTLib2Tweaks ExternalABC Source # 
Instance details

Defined in What4.Solver.ExternalABC

SMTLib2Tweaks STP Source # 
Instance details

Defined in What4.Solver.STP

SMTLib2Tweaks Z3 Source # 
Instance details

Defined in What4.Solver.Z3

SMTLib2Tweaks () Source # 
Instance details

Defined in What4.Protocol.SMTLib2

newWriter Source #

Arguments

:: a 
-> OutputStream Text

Stream to write queries onto

-> InputStream Text

Input stream to read responses from (may be the nullInput stream if no responses are expected)

-> AcknowledgementAction t (Writer a)

Action to run for consuming acknowledgement messages

-> ResponseStrictness

Be strict in parsing SMT solver responses?

-> String

Name of solver for reporting purposes.

-> Bool

Flag indicating if it is permitted to use "define-fun" when generating SMTLIB

-> ProblemFeatures

Indicates what features are supported by the solver

-> Bool

Indicates if quantifiers are supported.

-> SymbolVarBimap t

Variable bindings for names.

-> IO (WriterConn t (Writer a)) 

writeCheckSat :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO () Source #

Write check sat command

writeGetAbduct :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Text -> Term -> IO () Source #

writeCheckSynth :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO () Source #

Write check-synth command

runCheckSat Source #

Arguments

:: SMTLib2Tweaks b 
=> Session t b 
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)

Function for evaluating model. The evaluation should be complete before

-> IO a 

This function runs a check sat command

runGetAbducts :: SMTLib2Tweaks a => Session t a -> Int -> Text -> Term -> IO [String] Source #

runGetAbducts s nm p n, returns n formulas (as strings) the disjunction of which entails p (along with all the assertions in the context)

asSMT2Type :: forall a (tp :: BaseType). SMTLib2Tweaks a => TypeMap tp -> Sort Source #

setOption :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Text -> Text -> IO () Source #

versionResult :: WriterConn t a -> IO Text Source #

Get the result of a version query

nameResult :: WriterConn t a -> IO Text Source #

Get the result of a version query

setProduceModels :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Bool -> IO () Source #

Set the produce models option (We typically want this)

parseFnModel :: forall sym t (st :: Type -> Type) fs h. sym ~ ExprBuilder t st fs => sym -> WriterConn t h -> [SomeSymFn sym] -> SExp -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym)) Source #

parseFnValues :: forall sym t (st :: Type -> Type) fs h. sym ~ ExprBuilder t st fs => sym -> WriterConn t h -> [SomeSymFn sym] -> SExp -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym)) Source #

Logic

newtype Logic Source #

Identifies the set of predefined sorts and operators available.

Constructors

Logic Builder 

qf_bv :: Logic Source #

Use the QF_BV logic

allSupported :: Logic Source #

Deprecated: Use allLogic instead

Set the logic to all supported logics.

hornLogic :: Logic Source #

Use the Horn logic

all_supported :: Logic Source #

Deprecated: Use allLogic instead

Set the logic to all supported logics.

Type

newtype Sort Source #

Sort for SMTLIB expressions

Constructors

Sort 

Fields

arraySort :: Sort -> Sort -> Sort Source #

arraySort a b denotes the set of functions from a to be b.

Term

newtype Term Source #

Denotes an expression in the SMT solver

Constructors

T 

Fields

Instances

Instances details
IsString Term Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Syntax

Methods

fromString :: String -> Term

Monoid Term Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Syntax

Methods

mempty :: Term

mappend :: Term -> Term -> Term

mconcat :: [Term] -> Term

Semigroup Term Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Syntax

Methods

(<>) :: Term -> Term -> Term

sconcat :: NonEmpty Term -> Term

stimes :: Integral b => b -> Term -> Term

Num Term 
Instance details

Defined in What4.Protocol.SMTLib2

Methods

(+) :: Term -> Term -> Term

(-) :: Term -> Term -> Term

(*) :: Term -> Term -> Term

negate :: Term -> Term

abs :: Term -> Term

signum :: Term -> Term

fromInteger :: Integer -> Term

SupportTermOps Term Source # 
Instance details

Defined in What4.Protocol.SMTLib2

Methods

boolExpr :: Bool -> Term Source #

notExpr :: Term -> Term Source #

andAll :: [Term] -> Term Source #

orAll :: [Term] -> Term Source #

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

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

(.==) :: Term -> Term -> Term Source #

(./=) :: Term -> Term -> Term Source #

impliesExpr :: Term -> Term -> Term Source #

letExpr :: [(Text, Term)] -> Term -> Term Source #

ite :: Term -> Term -> Term -> Term Source #

sumExpr :: [Term] -> Term Source #

termIntegerToReal :: Term -> Term Source #

termRealToInteger :: Term -> Term Source #

integerTerm :: Integer -> Term Source #

rationalTerm :: Rational -> Term Source #

(.<=) :: Term -> Term -> Term Source #

(.<) :: Term -> Term -> Term Source #

(.>) :: Term -> Term -> Term Source #

(.>=) :: Term -> Term -> Term Source #

intAbs :: Term -> Term Source #

intDiv :: Term -> Term -> Term Source #

intMod :: Term -> Term -> Term Source #

intDivisible :: Term -> Natural -> Term Source #

bvTerm :: forall (w :: Nat). NatRepr w -> BV w -> Term Source #

bvNeg :: Term -> Term Source #

bvAdd :: Term -> Term -> Term Source #

bvSub :: Term -> Term -> Term Source #

bvMul :: Term -> Term -> Term Source #

bvSLe :: Term -> Term -> Term Source #

bvULe :: Term -> Term -> Term Source #

bvSLt :: Term -> Term -> Term Source #

bvULt :: Term -> Term -> Term Source #

bvUDiv :: Term -> Term -> Term Source #

bvURem :: Term -> Term -> Term Source #

bvSDiv :: Term -> Term -> Term Source #

bvSRem :: Term -> Term -> Term Source #

bvAnd :: Term -> Term -> Term Source #

bvOr :: Term -> Term -> Term Source #

bvXor :: Term -> Term -> Term Source #

bvNot :: Term -> Term Source #

bvShl :: Term -> Term -> Term Source #

bvLshr :: Term -> Term -> Term Source #

bvAshr :: Term -> Term -> Term Source #

bvConcat :: Term -> Term -> Term Source #

bvExtract :: forall (w :: Nat). NatRepr w -> Natural -> Natural -> Term -> Term Source #

bvTestBit :: forall (w :: Nat). NatRepr w -> Natural -> Term -> Term Source #

bvSumExpr :: forall (w :: Nat). NatRepr w -> [Term] -> Term Source #

floatTerm :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> BigFloat -> Term Source #

floatNeg :: Term -> Term Source #

floatAbs :: Term -> Term Source #

floatSqrt :: RoundingMode -> Term -> Term Source #

floatAdd :: RoundingMode -> Term -> Term -> Term Source #

floatSub :: RoundingMode -> Term -> Term -> Term Source #

floatMul :: RoundingMode -> Term -> Term -> Term Source #

floatDiv :: RoundingMode -> Term -> Term -> Term Source #

floatRem :: Term -> Term -> Term Source #

floatFMA :: RoundingMode -> Term -> Term -> Term -> Term Source #

floatEq :: Term -> Term -> Term Source #

floatFpEq :: Term -> Term -> Term Source #

floatLe :: Term -> Term -> Term Source #

floatLt :: Term -> Term -> Term Source #

floatIsNaN :: Term -> Term Source #

floatIsInf :: Term -> Term Source #

floatIsZero :: Term -> Term Source #

floatIsPos :: Term -> Term Source #

floatIsNeg :: Term -> Term Source #

floatIsSubnorm :: Term -> Term Source #

floatIsNorm :: Term -> Term Source #

floatCast :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatRound :: RoundingMode -> Term -> Term Source #

floatFromBinary :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> Term -> Term Source #

bvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

sbvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

realToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatToBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToSBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToReal :: Term -> Term Source #

realIsInteger :: Term -> Term Source #

realDiv :: Term -> Term -> Term Source #

realSin :: Term -> Term Source #

realCos :: Term -> Term Source #

realTan :: Term -> Term Source #

realATan2 :: Term -> Term -> Term Source #

realSinh :: Term -> Term Source #

realCosh :: Term -> Term Source #

realTanh :: Term -> Term Source #

realExp :: Term -> Term Source #

realLog :: Term -> Term Source #

smtFnApp :: Term -> [Term] -> Term Source #

smtFnUpdate :: Maybe (Term -> [Term] -> Term -> Term) Source #

lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> Term -> Term) Source #

fromText :: Text -> Term Source #

Solvers and External interface

data Session t a Source #

This is an interactive session with an SMT solver

Constructors

Session 

Fields

class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where Source #

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. a -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. a -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: a -> ProblemFeatures Source #

getErrorBehavior :: a -> WriterConn t (Writer a) -> IO ErrorBehavior Source #

supportsResetAssertions :: a -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer a) -> IO () Source #

newDefaultWriter Source #

Arguments

:: forall t (st :: Type -> Type) fs. a 
-> AcknowledgementAction t (Writer a) 
-> ProblemFeatures 
-> Maybe (ConfigOption BaseBoolType)

strictness override configuration

-> ExprBuilder t st fs 
-> OutputStream Text 
-> InputStream Text 
-> IO (WriterConn t (Writer a)) 

withSolver Source #

Arguments

:: forall t (st :: Type -> Type) fs b. a 
-> AcknowledgementAction t (Writer a) 
-> ProblemFeatures 
-> Maybe (ConfigOption BaseBoolType)

strictness override configuration

-> ExprBuilder t st fs 
-> FilePath

Path to solver executable

-> LogData 
-> (Session t a -> IO b)

Action to run

-> IO b 

Run the solver in a session.

runSolverInOverride Source #

Arguments

:: forall t (st :: Type -> Type) fs b. a 
-> AcknowledgementAction t (Writer a) 
-> ProblemFeatures 
-> Maybe (ConfigOption BaseBoolType)

strictness override configuration

-> ExprBuilder t st fs 
-> LogData 
-> [BoolExpr t] 
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) 
-> IO b 

Instances

Instances details
SMTLib2GenericSolver Bitwuzla Source # 
Instance details

Defined in What4.Solver.Bitwuzla

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. Bitwuzla -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. Bitwuzla -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: Bitwuzla -> ProblemFeatures Source #

getErrorBehavior :: Bitwuzla -> WriterConn t (Writer Bitwuzla) -> IO ErrorBehavior Source #

supportsResetAssertions :: Bitwuzla -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer Bitwuzla) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. Bitwuzla -> AcknowledgementAction t (Writer Bitwuzla) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer Bitwuzla)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. Bitwuzla -> AcknowledgementAction t (Writer Bitwuzla) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t Bitwuzla -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. Bitwuzla -> AcknowledgementAction t (Writer Bitwuzla) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

SMTLib2GenericSolver Boolector Source # 
Instance details

Defined in What4.Solver.Boolector

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. Boolector -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. Boolector -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: Boolector -> ProblemFeatures Source #

getErrorBehavior :: Boolector -> WriterConn t (Writer Boolector) -> IO ErrorBehavior Source #

supportsResetAssertions :: Boolector -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer Boolector) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer Boolector)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t Boolector -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

SMTLib2GenericSolver CVC4 Source # 
Instance details

Defined in What4.Solver.CVC4

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. CVC4 -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. CVC4 -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: CVC4 -> ProblemFeatures Source #

getErrorBehavior :: CVC4 -> WriterConn t (Writer CVC4) -> IO ErrorBehavior Source #

supportsResetAssertions :: CVC4 -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer CVC4) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. CVC4 -> AcknowledgementAction t (Writer CVC4) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer CVC4)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. CVC4 -> AcknowledgementAction t (Writer CVC4) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t CVC4 -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. CVC4 -> AcknowledgementAction t (Writer CVC4) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

SMTLib2GenericSolver CVC5 Source # 
Instance details

Defined in What4.Solver.CVC5

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. CVC5 -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. CVC5 -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: CVC5 -> ProblemFeatures Source #

getErrorBehavior :: CVC5 -> WriterConn t (Writer CVC5) -> IO ErrorBehavior Source #

supportsResetAssertions :: CVC5 -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer CVC5) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. CVC5 -> AcknowledgementAction t (Writer CVC5) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer CVC5)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. CVC5 -> AcknowledgementAction t (Writer CVC5) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t CVC5 -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. CVC5 -> AcknowledgementAction t (Writer CVC5) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

SMTLib2GenericSolver ExternalABC Source # 
Instance details

Defined in What4.Solver.ExternalABC

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. ExternalABC -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. ExternalABC -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: ExternalABC -> ProblemFeatures Source #

getErrorBehavior :: ExternalABC -> WriterConn t (Writer ExternalABC) -> IO ErrorBehavior Source #

supportsResetAssertions :: ExternalABC -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer ExternalABC) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. ExternalABC -> AcknowledgementAction t (Writer ExternalABC) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer ExternalABC)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. ExternalABC -> AcknowledgementAction t (Writer ExternalABC) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t ExternalABC -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. ExternalABC -> AcknowledgementAction t (Writer ExternalABC) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

SMTLib2GenericSolver STP Source # 
Instance details

Defined in What4.Solver.STP

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. STP -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. STP -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: STP -> ProblemFeatures Source #

getErrorBehavior :: STP -> WriterConn t (Writer STP) -> IO ErrorBehavior Source #

supportsResetAssertions :: STP -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer STP) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. STP -> AcknowledgementAction t (Writer STP) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer STP)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. STP -> AcknowledgementAction t (Writer STP) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t STP -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. STP -> AcknowledgementAction t (Writer STP) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

SMTLib2GenericSolver Z3 Source # 
Instance details

Defined in What4.Solver.Z3

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. Z3 -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. Z3 -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: Z3 -> ProblemFeatures Source #

getErrorBehavior :: Z3 -> WriterConn t (Writer Z3) -> IO ErrorBehavior Source #

supportsResetAssertions :: Z3 -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer Z3) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. Z3 -> AcknowledgementAction t (Writer Z3) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer Z3)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. Z3 -> AcknowledgementAction t (Writer Z3) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t Z3 -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. Z3 -> AcknowledgementAction t (Writer Z3) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

writeDefaultSMT2 Source #

Arguments

:: forall a t (st :: Type -> Type) fs. SMTLib2Tweaks a 
=> a 
-> String

Name of solver for reporting.

-> ProblemFeatures

Features supported by solver

-> Maybe (ConfigOption BaseBoolType)

strictness override configuration

-> ExprBuilder t st fs 
-> Handle 
-> [BoolExpr t] 
-> IO () 

A default method for writing SMTLib2 problems without any solver-specific tweaks.

defaultFileWriter :: forall a t (st :: Type -> Type) fs. SMTLib2Tweaks a => a -> String -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> Handle -> IO (WriterConn t (Writer a)) Source #

startSolver Source #

Arguments

:: forall a t (st :: Type -> Type) fs. SMTLib2GenericSolver a 
=> a 
-> AcknowledgementAction t (Writer a)

Action for acknowledging command responses

-> (WriterConn t (Writer a) -> IO ())

Action for setting start-up-time options and logic

-> SolverGoalTimeout 
-> ProblemFeatures 
-> Maybe (ConfigOption BaseBoolType)

strictness override configuration

-> Maybe Handle 
-> ExprBuilder t st fs 
-> IO (SolverProcess t (Writer a)) 

shutdownSolver :: SMTLib2GenericSolver a => a -> SolverProcess t (Writer a) -> IO (ExitCode, Text) Source #

data SMTLib2Exception Source #

Instances

Instances details
Exception SMTLib2Exception Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Response

Methods

toException :: SMTLib2Exception -> SomeException

fromException :: SomeException -> Maybe SMTLib2Exception

displayException :: SMTLib2Exception -> String

Show SMTLib2Exception Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Response

Methods

showsPrec :: Int -> SMTLib2Exception -> ShowS

show :: SMTLib2Exception -> String

showList :: [SMTLib2Exception] -> ShowS

Solver version

ppSolverVersionCheckError :: SolverVersionCheckError -> Doc ann Source #

ppSolverVersionError :: SolverVersionError -> Doc ann Source #

checkSolverVersion :: SMTLib2Tweaks solver => SolverProcess scope (Writer solver) -> IO (Either SolverVersionCheckError (Maybe SolverVersionError)) Source #

Ensure the solver's version falls within a known-good range.

checkSolverVersion' :: SMTLib2Tweaks solver => Map Text SolverBounds -> SolverProcess scope (Writer solver) -> IO (Either SolverVersionCheckError (Maybe SolverVersionError)) Source #

Ensure the solver's version falls within a known-good range.

queryErrorBehavior :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ErrorBehavior Source #

Query the solver's error behavior setting

defaultSolverBounds :: Map Text SolverBounds Source #

Solver version bounds computed from "solverBounds.config"

Re-exports

assume :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO () Source #

Write assume formula predicates for asserting predicate holds.

supportedFeatures :: WriterConn t h -> ProblemFeatures Source #

Indicates features supported by the solver.

nullAcknowledgementAction :: AcknowledgementAction t h Source #

An acknowledgement action that does nothing

Orphan instances

Num Term Source # 
Instance details

Methods

(+) :: Term -> Term -> Term

(-) :: Term -> Term -> Term

(*) :: Term -> Term -> Term

negate :: Term -> Term

abs :: Term -> Term

signum :: Term -> Term

fromInteger :: Integer -> Term

SupportTermOps Term Source # 
Instance details

Methods

boolExpr :: Bool -> Term Source #

notExpr :: Term -> Term Source #

andAll :: [Term] -> Term Source #

orAll :: [Term] -> Term Source #

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

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

(.==) :: Term -> Term -> Term Source #

(./=) :: Term -> Term -> Term Source #

impliesExpr :: Term -> Term -> Term Source #

letExpr :: [(Text, Term)] -> Term -> Term Source #

ite :: Term -> Term -> Term -> Term Source #

sumExpr :: [Term] -> Term Source #

termIntegerToReal :: Term -> Term Source #

termRealToInteger :: Term -> Term Source #

integerTerm :: Integer -> Term Source #

rationalTerm :: Rational -> Term Source #

(.<=) :: Term -> Term -> Term Source #

(.<) :: Term -> Term -> Term Source #

(.>) :: Term -> Term -> Term Source #

(.>=) :: Term -> Term -> Term Source #

intAbs :: Term -> Term Source #

intDiv :: Term -> Term -> Term Source #

intMod :: Term -> Term -> Term Source #

intDivisible :: Term -> Natural -> Term Source #

bvTerm :: forall (w :: Nat). NatRepr w -> BV w -> Term Source #

bvNeg :: Term -> Term Source #

bvAdd :: Term -> Term -> Term Source #

bvSub :: Term -> Term -> Term Source #

bvMul :: Term -> Term -> Term Source #

bvSLe :: Term -> Term -> Term Source #

bvULe :: Term -> Term -> Term Source #

bvSLt :: Term -> Term -> Term Source #

bvULt :: Term -> Term -> Term Source #

bvUDiv :: Term -> Term -> Term Source #

bvURem :: Term -> Term -> Term Source #

bvSDiv :: Term -> Term -> Term Source #

bvSRem :: Term -> Term -> Term Source #

bvAnd :: Term -> Term -> Term Source #

bvOr :: Term -> Term -> Term Source #

bvXor :: Term -> Term -> Term Source #

bvNot :: Term -> Term Source #

bvShl :: Term -> Term -> Term Source #

bvLshr :: Term -> Term -> Term Source #

bvAshr :: Term -> Term -> Term Source #

bvConcat :: Term -> Term -> Term Source #

bvExtract :: forall (w :: Nat). NatRepr w -> Natural -> Natural -> Term -> Term Source #

bvTestBit :: forall (w :: Nat). NatRepr w -> Natural -> Term -> Term Source #

bvSumExpr :: forall (w :: Nat). NatRepr w -> [Term] -> Term Source #

floatTerm :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> BigFloat -> Term Source #

floatNeg :: Term -> Term Source #

floatAbs :: Term -> Term Source #

floatSqrt :: RoundingMode -> Term -> Term Source #

floatAdd :: RoundingMode -> Term -> Term -> Term Source #

floatSub :: RoundingMode -> Term -> Term -> Term Source #

floatMul :: RoundingMode -> Term -> Term -> Term Source #

floatDiv :: RoundingMode -> Term -> Term -> Term Source #

floatRem :: Term -> Term -> Term Source #

floatFMA :: RoundingMode -> Term -> Term -> Term -> Term Source #

floatEq :: Term -> Term -> Term Source #

floatFpEq :: Term -> Term -> Term Source #

floatLe :: Term -> Term -> Term Source #

floatLt :: Term -> Term -> Term Source #

floatIsNaN :: Term -> Term Source #

floatIsInf :: Term -> Term Source #

floatIsZero :: Term -> Term Source #

floatIsPos :: Term -> Term Source #

floatIsNeg :: Term -> Term Source #

floatIsSubnorm :: Term -> Term Source #

floatIsNorm :: Term -> Term Source #

floatCast :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatRound :: RoundingMode -> Term -> Term Source #

floatFromBinary :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> Term -> Term Source #

bvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

sbvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

realToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatToBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToSBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToReal :: Term -> Term Source #

realIsInteger :: Term -> Term Source #

realDiv :: Term -> Term -> Term Source #

realSin :: Term -> Term Source #

realCos :: Term -> Term Source #

realTan :: Term -> Term Source #

realATan2 :: Term -> Term -> Term Source #

realSinh :: Term -> Term Source #

realCosh :: Term -> Term Source #

realTanh :: Term -> Term Source #

realExp :: Term -> Term Source #

realLog :: Term -> Term Source #

smtFnApp :: Term -> [Term] -> Term Source #

smtFnUpdate :: Maybe (Term -> [Term] -> Term -> Term) Source #

lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> Term -> Term) Source #

fromText :: Text -> Term Source #