ROSE 0.11.145.147
|
Definition at line 234 of file SmtSolver.h.
Public Member Functions | |
operator bool () const | |
True if lookup was a cache hit. | |
Public Attributes | |
Sawyer::Optional< Satisfiable > | satisfiable |
If found, whether satisfiable. | |
ExprList | sortedNormalized |
Sorted and normalized assertions, regardless if found. | |
SymbolicExpression::ExprExprHashMap | rewriteMap |
Mapping from provided to sortedNormalized assertions. | |
ExprExprMap | evidence |
Normalized evidence if found and satisfiable. | |
|
inlineexplicit |
Sawyer::Optional<Satisfiable> Rose::BinaryAnalysis::SmtSolver::Memoizer::Found::satisfiable |
If found, whether satisfiable.
Definition at line 235 of file SmtSolver.h.
Referenced by operator bool().
ExprList Rose::BinaryAnalysis::SmtSolver::Memoizer::Found::sortedNormalized |
Sorted and normalized assertions, regardless if found.
Definition at line 236 of file SmtSolver.h.
SymbolicExpression::ExprExprHashMap Rose::BinaryAnalysis::SmtSolver::Memoizer::Found::rewriteMap |
Mapping from provided to sortedNormalized assertions.
Definition at line 237 of file SmtSolver.h.
ExprExprMap Rose::BinaryAnalysis::SmtSolver::Memoizer::Found::evidence |
Normalized evidence if found and satisfiable.
Definition at line 238 of file SmtSolver.h.