Crux.Config.Solver

Documentation

parseSolverConfig :: CruxOptions -> Either [String] SolverConfig

Examine a CruxOptions and determine what solver configuration to use for symbolic execution. This can fail if an invalid solver configuration is requested by the user.

The high level logic is that:

• If a user specifies only a single solver with the --solver option, that is used as an online solver if possible for path sat checking (if requested) and goal discharge.
• If the user specifies an explicit --path-sat-solver, that solver is used for path satisfiability checking (if requested) while the solver specified with --solver is used for goal discharge.
• The goal solver can be entirely offline (if it doesn't support online mode) or if the user requests that it be used in offline mode with the
• -force-offline-goal-solving option.

data SolverConfig

Constructors

SingleOnlineSolver SolverOnline

Use a single online solver for both path satisfiability checking and goal discharge

OnlineSolverWithOfflineGoals SolverOnline SolverOffline

Use an online solver for path satisfiability checking and use an offline solver for goal discharge

OnlineSolverWithSeparateOnlineGoals SolverOnline SolverOnline

Use one online solver connection for path satisfiability checking and a separate online solver connection for goal discharge. INVARIANT: the solvers must be distinct.

OnlyOfflineSolvers [SolverOffline]

Try any of a number of offline solvers with no support for path satisfiability checking

data SolverOnline

Constructors

Yices

Z3

CVC4

CVC5

STP

Instances

Show SolverOnline

Defined in Crux.Config.Solver

Methods

showsPrec :: Int -> SolverOnline -> ShowS

show :: SolverOnline -> String

showList :: [SolverOnline] -> ShowS

HasDefaultFloatRepr SolverOnline

Defined in Crux.Config.Solver

Methods

withDefaultFloatRepr :: st s -> SolverOnline -> (forall (fm :: FloatMode). IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) => FloatModeRepr fm -> a) -> a

Eq SolverOnline

Defined in Crux.Config.Solver

Methods

(==) :: SolverOnline -> SolverOnline -> Bool

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

Ord SolverOnline

Defined in Crux.Config.Solver

Methods

compare :: SolverOnline -> SolverOnline -> Ordering

(<) :: SolverOnline -> SolverOnline -> Bool

(<=) :: SolverOnline -> SolverOnline -> Bool

(>) :: SolverOnline -> SolverOnline -> Bool

(>=) :: SolverOnline -> SolverOnline -> Bool

max :: SolverOnline -> SolverOnline -> SolverOnline

min :: SolverOnline -> SolverOnline -> SolverOnline

data SolverOffline

Constructors

SolverOnline SolverOnline

Boolector

DReal

Instances

Show SolverOffline

Defined in Crux.Config.Solver

Methods

showsPrec :: Int -> SolverOffline -> ShowS

show :: SolverOffline -> String

showList :: [SolverOffline] -> ShowS

HasDefaultFloatRepr SolverOffline

Defined in Crux.Config.Solver

Methods

withDefaultFloatRepr :: st s -> SolverOffline -> (forall (fm :: FloatMode). IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) => FloatModeRepr fm -> a) -> a

Eq SolverOffline

Defined in Crux.Config.Solver

Methods

(==) :: SolverOffline -> SolverOffline -> Bool

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

Ord SolverOffline

Defined in Crux.Config.Solver

Methods

compare :: SolverOffline -> SolverOffline -> Ordering

(<) :: SolverOffline -> SolverOffline -> Bool

(<=) :: SolverOffline -> SolverOffline -> Bool

(>) :: SolverOffline -> SolverOffline -> Bool

(>=) :: SolverOffline -> SolverOffline -> Bool

max :: SolverOffline -> SolverOffline -> SolverOffline

min :: SolverOffline -> SolverOffline -> SolverOffline

class HasDefaultFloatRepr solver where

Methods

withDefaultFloatRepr :: st s -> solver -> (forall fm. IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) => FloatModeRepr fm -> a) -> a

Instances

HasDefaultFloatRepr SolverOffline

Defined in Crux.Config.Solver

Methods

withDefaultFloatRepr :: st s -> SolverOffline -> (forall (fm :: FloatMode). IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) => FloatModeRepr fm -> a) -> a

HasDefaultFloatRepr SolverOnline

Defined in Crux.Config.Solver

Methods

withDefaultFloatRepr :: st s -> SolverOnline -> (forall (fm :: FloatMode). IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) => FloatModeRepr fm -> a) -> a

sameSolver :: SolverOnline -> SolverOffline -> Bool

Test to see if an online and offline solver are actually the same