| Copyright | (c) Galois Inc 2024 |
|---|---|
| License | BSD3 |
| Maintainer | Langston Barrett <langston@galois.com> |
| Stability | provisional |
| Safe Haskell | None |
| Language | Haskell2010 |
What4.Concretize
Description
In our terminology, concretization is the process of (1) obtaining a model from an SMT solver and (2) requesting the value of a particular set of symbolic expressions in said model. The operation (2) alone is called "grounding", see What4.GroundEval.
Synopsis
- data ConcretizationFailure
- concretize :: forall sym scope (st :: Type -> Type) fs solver (tp :: BaseType). (sym ~ ExprBuilder scope st fs, OnlineSolver solver) => SolverProcess scope solver -> SymExpr sym tp -> IO (Either ConcretizationFailure (GroundValue tp))
- data UniqueConcretizationFailure
- uniquelyConcretize :: forall sym scope (st :: Type -> Type) fs solver (tp :: BaseType). (sym ~ ExprBuilder scope st fs, OnlineSolver solver) => sym -> SolverProcess scope solver -> SymExpr sym tp -> IO (Either UniqueConcretizationFailure (GroundValue tp))
Documentation
data ConcretizationFailure Source #
Reasons why attempting to resolve a symbolic expression as ground can fail.
Constructors
| SolverUnknown | Querying the SMT solver yielded |
| UnsatInitialAssumptions | Querying the SMT solver for an initial model of the expression failed due to the initial assumptions in scope being unsatisfiable. |
Instances
| Show ConcretizationFailure Source # | |
Defined in What4.Concretize Methods showsPrec :: Int -> ConcretizationFailure -> ShowS # show :: ConcretizationFailure -> String # showList :: [ConcretizationFailure] -> ShowS # | |
Arguments
| :: forall sym scope (st :: Type -> Type) fs solver (tp :: BaseType). (sym ~ ExprBuilder scope st fs, OnlineSolver solver) | |
| => SolverProcess scope solver | |
| -> SymExpr sym tp | The symbolic term to query from the model |
| -> IO (Either ConcretizationFailure (GroundValue tp)) |
Get a GroundValue for a SymExpr by asking an online solver for
a model.
In contrast with uniquelyConcretize, this function returns the value of the
SymExpr in just one of potentially many distinct models. See the Haddock
on uniquelyConcretize for a further comparison.
data UniqueConcretizationFailure Source #
Constructors
| GroundingFailure ConcretizationFailure | |
| MultipleModels | There are multiple possible models for the expression, which means it is truly symbolic and therefore unable to be uniquely concretized. |
Instances
| Show UniqueConcretizationFailure Source # | |
Defined in What4.Concretize Methods showsPrec :: Int -> UniqueConcretizationFailure -> ShowS # show :: UniqueConcretizationFailure -> String # showList :: [UniqueConcretizationFailure] -> ShowS # | |
Arguments
| :: forall sym scope (st :: Type -> Type) fs solver (tp :: BaseType). (sym ~ ExprBuilder scope st fs, OnlineSolver solver) | |
| => sym | The symbolic backend |
| -> SolverProcess scope solver | |
| -> SymExpr sym tp | The symbolic term to concretize |
| -> IO (Either UniqueConcretizationFailure (GroundValue tp)) |
Attempt to resolve the given SymExpr to a unique concrete value using
an online SMT solver connection.
The implementation of this function (1) asks for a model from the solver.
If it gets one, it (2) adds a blocking clause and asks for another. If there
was only one model, concretize the initial value and return it with Right.
Otherwise, return an explanation of why concretization failed with Left.
This behavior is contrasted with concretize, which just does (1).