Description
Memoizes calls to an SMT solver.
This class memoizes calls to the check function for a particular SMT solver, or across some collection of solvers. For every non-trivial call to check, the memoizer caches the input set of assertions and the output satisfiability and, if satisfiable, the output evidence of satisfiability. Moreover, it does this in such a way that assertions that only vary in their variable names can be matched to previously cached calls.
In order to use memoization, a non-null memoizer should be passed to the SmtSolver::instance factory, or a non-null memoizer pointer should be assigned to the memoizer property of the SmtSolver. To disable memoization, assign a null pointer to the memoizer property. Multiple SmtSolver objects can share the same memoizer, but this should generally only be done when all such solvers are guaranteed to return the same values for any given inputs, which is not always the case due to differences in implementation.
In order to match calls whose inputs vary only in order of assertions and/or variable names, the assertions are sorted and normalized before being stored in the cache. First, to sort the assertions each assertion is independently normalized by renaming its variables starting at "v0" in the order they're encountered in a depth-first-search traversal. Then the input assertions are sorted according to the hashes of their corresponding normalized versions. Finally, the variables in the sorted assertions are collectively renamed, producing a sorted-normalized set of assertions and a renaming map. When a new result is added to the cache, the variables in the evidence of satisfiability are renamed according to renaming map. The original assertions, original evidence of satisfiability, and renaming map are discarded. When a cache hit occurs and the evidence needs to be returned, the cached evidence is de-normalized using the inverse of the temporary renaming map for the current input assertions.
Thread safety: All member functions are thread safe unless otherwise noted.
Definition at line 228 of file SmtSolver.h.
#include <Rose/BinaryAnalysis/SmtSolver.h>
Classes | |
| struct | Found |
Public Types | |
| using | Ptr = Sawyer::SharedPointer< Memoizer > |
| Reference counting pointer. | |
Public Member Functions | |
| void | clear () |
| Clear the entire cache as if it was just constructed. | |
| Found | find (const ExprList &assertions) |
| Search for the specified assertions in the cache. | |
| ExprExprMap | evidence (const Found &) const |
| Returns evidence of satisfiability. | |
| void | insert (const Found &, Satisfiable, const ExprExprMap &evidence) |
| Insert a call record into the cache. | |
| size_t | size () const |
| Number of call records cached. | |
| Map::iterator | searchNS (SymbolicExpression::Hash, const ExprList &sortedNormalized) |
 Public Member Functions inherited from Sawyer::SharedObject | |
| SharedObject () | |
| Default constructor. | |
| SharedObject (const SharedObject &) | |
| Copy constructor. | |
| virtual | ~SharedObject () |
| Virtual destructor. | |
| SharedObject & | operator= (const SharedObject &) |
| Assignment. | |
Static Public Member Functions | |
| static Ptr | instance () |
| Allocating constructor. | |
Member Typedef Documentation
◆ Ptr
Reference counting pointer.
Definition at line 231 of file SmtSolver.h.
Constructor & Destructor Documentation
◆ Memoizer()
|
inlineprotected |
Definition at line 264 of file SmtSolver.h.
Member Function Documentation
◆ find()
Search for the specified assertions in the cache.
If this is a cache hit, then the return value evaluates to true in Boolean context and contains the satisfiability and normalized evidence. The evidence needs to be de-normalized by the evidence function before it can be used. If this is a cache miss, then the return value evaluates to false in Boolean context, but it contains enough information for the SMT solver results to be inserted into the cache later by the insert function.
The documentation for this class describes how the search works by sorting and normalizing the input assertions.
◆ evidence()
| ExprExprMap Rose::BinaryAnalysis::SmtSolver::Memoizer::evidence | ( | const Found & | ) | const |
Returns evidence of satisfiability.
The argument is the result from find. If the argument evaluates to true in Boolean context (i.e., the find was a cache hit) then this function will de-normalize the cached evidence of satisfiability and return it. This function should not be called if the argument evaluates to false in a Boolean context (i.e., the find was a cache miss).
◆ insert()
| void Rose::BinaryAnalysis::SmtSolver::Memoizer::insert | ( | const Found & | , |
| Satisfiable | , | ||
| const ExprExprMap & | evidence | ||
| ) |
Insert a call record into the cache.
The first argument is the return value from find which must have been a cache miss. The remaining arguments are the results from the SMT solver for the same assertions that were used in the find call. The evidence is normalized using the same variable mapping as was used for the input assertions during the find call, and then stored in the cache in normalized form.
The documentation for this class was generated from the following file:
